Metamath Proof Explorer


Theorem enpr2d

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 φAC
enpr2d.2 φBD
enpr2d.3 φ¬A=B
Assertion enpr2d φAB2𝑜

Proof

Step Hyp Ref Expression
1 enpr2d.1 φAC
2 enpr2d.2 φBD
3 enpr2d.3 φ¬A=B
4 0ex V
5 4 a1i φV
6 1oex 1𝑜V
7 6 a1i φ1𝑜V
8 3 neqned φAB
9 1n0 1𝑜
10 9 necomi 1𝑜
11 10 a1i φ1𝑜
12 1 2 5 7 8 11 en2prd φAB1𝑜
13 df2o3 2𝑜=1𝑜
14 12 13 breqtrrdi φAB2𝑜