Metamath Proof Explorer


Theorem en2sn

Description: Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024)

Ref Expression
Assertion en2sn A C B D A B

Proof

Step Hyp Ref Expression
1 snex A B V
2 f1osng A C B D A B : A 1-1 onto B
3 f1oeq1 f = A B f : A 1-1 onto B A B : A 1-1 onto B
4 3 spcegv A B V A B : A 1-1 onto B f f : A 1-1 onto B
5 1 2 4 mpsyl A C B D f f : A 1-1 onto B
6 bren A B f f : A 1-1 onto B
7 5 6 sylibr A C B D A B