Description: A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023) Avoid ax-un . (Revised by BTernaryTau, 23-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | enpr2d.1 | |
|
enpr2d.2 | |
||
enpr2d.3 | |
||
Assertion | enpr2d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enpr2d.1 | |
|
2 | enpr2d.2 | |
|
3 | enpr2d.3 | |
|
4 | 0ex | |
|
5 | 4 | a1i | |
6 | 1oex | |
|
7 | 6 | a1i | |
8 | 3 | neqned | |
9 | 1n0 | |
|
10 | 9 | necomi | |
11 | 10 | a1i | |
12 | 1 2 5 7 8 11 | en2prd | |
13 | df2o3 | |
|
14 | 12 13 | breqtrrdi | |