Theorem enpr2

Description: An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d . (Contributed by FL, 17-Aug-2008) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 30-Dec-2024)

	Ref	Expression
Assertion	enpr2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )

Proof

Step	Hyp	Ref	Expression
1		df-ne	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )
2		simp1	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝐶 )
3		simp2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝐷 )
4		simp3	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐴 = 𝐵 )
5	2 3 4	enpr2d	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 = 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
6	1 5	syl3an3b	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )