Theorem pr2eldif1

Description: If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023)

	Ref	Expression
Assertion	pr2eldif1	⊢ ( { 𝐴 , 𝐵 } ≈ 2o → 𝐴 ∈ ( { 𝐴 , 𝐵 } ∖ { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		pren2	⊢ ( { 𝐴 , 𝐵 } ≈ 2o ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) )
2		prid1g	⊢ ( 𝐴 ∈ V → 𝐴 ∈ { 𝐴 , 𝐵 } )
3	2	3ad2ant1	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
4		nelsn	⊢ ( 𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ { 𝐵 } )
5	4	3ad2ant3	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ¬ 𝐴 ∈ { 𝐵 } )
6	3 5	eldifd	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ( { 𝐴 , 𝐵 } ∖ { 𝐵 } ) )
7	1 6	sylbi	⊢ ( { 𝐴 , 𝐵 } ≈ 2o → 𝐴 ∈ ( { 𝐴 , 𝐵 } ∖ { 𝐵 } ) )