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	|- ( { A , B } ~~ 2o -> A e. ( { A , B } \ { B } ) )

Proof

Step	Hyp	Ref	Expression
1		pren2	|- ( { A , B } ~~ 2o <-> ( A e. _V /\ B e. _V /\ A =/= B ) )
2		prid1g	|- ( A e. _V -> A e. { A , B } )
3	2	3ad2ant1	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) -> A e. { A , B } )
4		nelsn	|- ( A =/= B -> -. A e. { B } )
5	4	3ad2ant3	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) -> -. A e. { B } )
6	3 5	eldifd	|- ( ( A e. _V /\ B e. _V /\ A =/= B ) -> A e. ( { A , B } \ { B } ) )
7	1 6	sylbi	|- ( { A , B } ~~ 2o -> A e. ( { A , B } \ { B } ) )