Metamath Proof Explorer

Theorem prnebg

Description: A (proper) pair is not equal to another (maybe improper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018)

Ref Expression
Assertion prnebg 
|- ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) <-> { A , B } =/= { C , D } ) )

Proof

Step Hyp Ref Expression
1 prneimg 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) -> { A , B } =/= { C , D } ) )
2 1 3adant3 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) -> { A , B } =/= { C , D } ) )
3 ioran 
 |-  ( -. ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) <-> ( -. ( A =/= C /\ A =/= D ) /\ -. ( B =/= C /\ B =/= D ) ) )
4 ianor 
 |-  ( -. ( A =/= C /\ A =/= D ) <-> ( -. A =/= C \/ -. A =/= D ) )
5 nne 
 |-  ( -. A =/= C <-> A = C )
6 nne 
 |-  ( -. A =/= D <-> A = D )
7 5 6 orbi12i 
 |-  ( ( -. A =/= C \/ -. A =/= D ) <-> ( A = C \/ A = D ) )
8 4 7 bitri 
 |-  ( -. ( A =/= C /\ A =/= D ) <-> ( A = C \/ A = D ) )
9 ianor 
 |-  ( -. ( B =/= C /\ B =/= D ) <-> ( -. B =/= C \/ -. B =/= D ) )
10 nne 
 |-  ( -. B =/= C <-> B = C )
11 nne 
 |-  ( -. B =/= D <-> B = D )
12 10 11 orbi12i 
 |-  ( ( -. B =/= C \/ -. B =/= D ) <-> ( B = C \/ B = D ) )
13 9 12 bitri 
 |-  ( -. ( B =/= C /\ B =/= D ) <-> ( B = C \/ B = D ) )
14 8 13 anbi12i 
 |-  ( ( -. ( A =/= C /\ A =/= D ) /\ -. ( B =/= C /\ B =/= D ) ) <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) )
15 3 14 bitri 
 |-  ( -. ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) )
16 anddi 
 |-  ( ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) <-> ( ( ( A = C /\ B = C ) \/ ( A = C /\ B = D ) ) \/ ( ( A = D /\ B = C ) \/ ( A = D /\ B = D ) ) ) )
17 eqtr3 
 |-  ( ( A = C /\ B = C ) -> A = B )
18 eqneqall 
 |-  ( A = B -> ( A =/= B -> { A , B } = { C , D } ) )
19 17 18 syl 
 |-  ( ( A = C /\ B = C ) -> ( A =/= B -> { A , B } = { C , D } ) )
20 preq12 
 |-  ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
21 20 a1d 
 |-  ( ( A = C /\ B = D ) -> ( A =/= B -> { A , B } = { C , D } ) )
22 19 21 jaoi 
 |-  ( ( ( A = C /\ B = C ) \/ ( A = C /\ B = D ) ) -> ( A =/= B -> { A , B } = { C , D } ) )
23 preq12 
 |-  ( ( A = D /\ B = C ) -> { A , B } = { D , C } )
24 prcom 
 |-  { D , C } = { C , D }
25 23 24 eqtrdi 
 |-  ( ( A = D /\ B = C ) -> { A , B } = { C , D } )
26 25 a1d 
 |-  ( ( A = D /\ B = C ) -> ( A =/= B -> { A , B } = { C , D } ) )
27 eqtr3 
 |-  ( ( A = D /\ B = D ) -> A = B )
28 27 18 syl 
 |-  ( ( A = D /\ B = D ) -> ( A =/= B -> { A , B } = { C , D } ) )
29 26 28 jaoi 
 |-  ( ( ( A = D /\ B = C ) \/ ( A = D /\ B = D ) ) -> ( A =/= B -> { A , B } = { C , D } ) )
30 22 29 jaoi 
 |-  ( ( ( ( A = C /\ B = C ) \/ ( A = C /\ B = D ) ) \/ ( ( A = D /\ B = C ) \/ ( A = D /\ B = D ) ) ) -> ( A =/= B -> { A , B } = { C , D } ) )
31 30 com12 
 |-  ( A =/= B -> ( ( ( ( A = C /\ B = C ) \/ ( A = C /\ B = D ) ) \/ ( ( A = D /\ B = C ) \/ ( A = D /\ B = D ) ) ) -> { A , B } = { C , D } ) )
32 31 3ad2ant3 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( ( ( ( A = C /\ B = C ) \/ ( A = C /\ B = D ) ) \/ ( ( A = D /\ B = C ) \/ ( A = D /\ B = D ) ) ) -> { A , B } = { C , D } ) )
33 16 32 syl5bi 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) -> { A , B } = { C , D } ) )
34 15 33 syl5bi 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( -. ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) -> { A , B } = { C , D } ) )
35 34 necon1ad 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( { A , B } =/= { C , D } -> ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) ) )
36 2 35 impbid 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) <-> { A , B } =/= { C , D } ) )