Theorem en2pr

Description: A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023)

	Ref	Expression
Assertion	en2pr	⊢ ( 𝐴 ≈ 2o ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝑥 ≠ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		en2	⊢ ( 𝐴 ≈ 2o → ∃ 𝑥 ∃ 𝑦 𝐴 = { 𝑥 , 𝑦 } )
2	1	pm4.71ri	⊢ ( 𝐴 ≈ 2o ↔ ( ∃ 𝑥 ∃ 𝑦 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐴 ≈ 2o ) )
3		19.41vv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐴 ≈ 2o ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐴 ≈ 2o ) )
4		breq1	⊢ ( 𝐴 = { 𝑥 , 𝑦 } → ( 𝐴 ≈ 2o ↔ { 𝑥 , 𝑦 } ≈ 2o ) )
5		pr2ne	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( { 𝑥 , 𝑦 } ≈ 2o ↔ 𝑥 ≠ 𝑦 ) )
6	5	el2v	⊢ ( { 𝑥 , 𝑦 } ≈ 2o ↔ 𝑥 ≠ 𝑦 )
7	4 6	bitrdi	⊢ ( 𝐴 = { 𝑥 , 𝑦 } → ( 𝐴 ≈ 2o ↔ 𝑥 ≠ 𝑦 ) )
8	7	pm5.32i	⊢ ( ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐴 ≈ 2o ) ↔ ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝑥 ≠ 𝑦 ) )
9	8	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐴 ≈ 2o ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝑥 ≠ 𝑦 ) )
10	2 3 9	3bitr2i	⊢ ( 𝐴 ≈ 2o ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝑥 ≠ 𝑦 ) )