Theorem pr2eldif2

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	pr2eldif2	⊢ ( { 𝐴 , 𝐵 } ≈ 2o → 𝐵 ∈ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) )

Proof

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