and exploiting the connection between X ~ Y and injections, and the connection between xy and equality.

Assume a class has size m, but also has size k;
show m must actually be k.
Each direction of the equality, namely,

mk and km,

may be proved in the same way, so we generalize the goal slightly to

x,y:. (x ~ y) xy.

Once this is proved, mk and km follow easily from it since m ~ k and k ~ m follow easily from our assumptions and the fact that X ~ Y is an equivalence relation, i.e.,