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

Proof

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