Description: Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | en2sn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snex | ||
2 | f1osng | ||
3 | f1oeq1 | ||
4 | 3 | spcegv | |
5 | 1 2 4 | mpsyl | |
6 | bren | ||
7 | 5 6 | sylibr |