Theorem pren2

Description: An unordered pair is equinumerous to ordinal two iff both parts are sets not equal to each other. (Contributed by RP, 8-Oct-2023)

	Ref	Expression
Assertion	pren2	⊢ ( { 𝐴 , 𝐵 } ≈ 2o ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		pr2ne	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( { 𝐴 , 𝐵 } ≈ 2o ↔ 𝐴 ≠ 𝐵 ) )
2	1	pm5.32i	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ { 𝐴 , 𝐵 } ≈ 2o ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 ≠ 𝐵 ) )
3		pr2cv	⊢ ( { 𝐴 , 𝐵 } ≈ 2o → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4	3	pm4.71ri	⊢ ( { 𝐴 , 𝐵 } ≈ 2o ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ { 𝐴 , 𝐵 } ≈ 2o ) )
5		df-3an	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 ≠ 𝐵 ) )
6	2 4 5	3bitr4i	⊢ ( { 𝐴 , 𝐵 } ≈ 2o ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) )