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	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
	enpr2d.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	enpr2d.3	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
Assertion	enpr2d	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ 2o )

Proof

Step	Hyp	Ref	Expression
1		enpr2d.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
2		enpr2d.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
3		enpr2d.3	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
4		0ex	⊢ ∅ ∈ V
5	4	a1i	⊢ ( 𝜑 → ∅ ∈ V )
6		1oex	⊢ 1o ∈ V
7	6	a1i	⊢ ( 𝜑 → 1o ∈ V )
8	3	neqned	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
9		1n0	⊢ 1o ≠ ∅
10	9	necomi	⊢ ∅ ≠ 1o
11	10	a1i	⊢ ( 𝜑 → ∅ ≠ 1o )
12	1 2 5 7 8 11	en2prd	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ { ∅ , 1o } )
13		df2o3	⊢ 2o = { ∅ , 1o }
14	12 13	breqtrrdi	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ 2o )