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 φ A C
enpr2d.2 φ B D
enpr2d.3 φ ¬ A = B
Assertion enpr2d φ A B 2 𝑜

Proof

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