Metamath Proof Explorer

Theorem pr2nelemOLD

Description: Obsolete version of enpr2 as of 30-Dec-2024. (Contributed by FL, 17-Aug-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pr2nelemOLD 
|- ( ( 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 )