Description: A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | en2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1on | ||
2 | 1 | onordi | |
3 | df-2o | ||
4 | en1 | ||
5 | 4 | biimpi | |
6 | df-pr | ||
7 | 6 | enp1ilem | |
8 | 7 | eximdv | |
9 | 2 3 5 8 | enp1i |