Theorem pr2nelem

Description: Lemma for pr2ne . (Contributed by FL, 17-Aug-2008)

	Ref	Expression
Assertion	pr2nelem	|- ( ( A e. C /\ B e. D /\ A =/= B ) -> { A , B } ~~ 2o )

Proof

Step	Hyp	Ref	Expression
1		disjsn2	|- ( A =/= B -> ( { A } i^i { B } ) = (/) )
2		ensn1g	|- ( A e. C -> { A } ~~ 1o )
3		ensn1g	|- ( B e. D -> { B } ~~ 1o )
4		pm54.43	|- ( ( { A } ~~ 1o /\ { B } ~~ 1o ) -> ( ( { A } i^i { B } ) = (/) <-> ( { A } u. { B } ) ~~ 2o ) )
5		df-pr	|- { A , B } = ( { A } u. { B } )
6	5	breq1i	|- ( { A , B } ~~ 2o <-> ( { A } u. { B } ) ~~ 2o )
7	4 6	bitr4di	|- ( ( { A } ~~ 1o /\ { B } ~~ 1o ) -> ( ( { A } i^i { B } ) = (/) <-> { A , B } ~~ 2o ) )
8	7	biimpd	|- ( ( { A } ~~ 1o /\ { B } ~~ 1o ) -> ( ( { A } i^i { B } ) = (/) -> { A , B } ~~ 2o ) )
9	2 3 8	syl2an	|- ( ( A e. C /\ B e. D ) -> ( ( { A } i^i { B } ) = (/) -> { A , B } ~~ 2o ) )
10	9	ex	|- ( A e. C -> ( B e. D -> ( ( { A } i^i { B } ) = (/) -> { A , B } ~~ 2o ) ) )
11	1 10	syl7	|- ( A e. C -> ( B e. D -> ( A =/= B -> { A , B } ~~ 2o ) ) )
12	11	3imp	|- ( ( A e. C /\ B e. D /\ A =/= B ) -> { A , B } ~~ 2o )