Metamath Proof Explorer

Theorem prneimg

Description: Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017)

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

Proof

Step Hyp Ref Expression
1 preq12bg 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
2 orddi 
 |-  ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) <-> ( ( ( A = C \/ A = D ) /\ ( A = C \/ B = C ) ) /\ ( ( B = D \/ A = D ) /\ ( B = D \/ B = C ) ) ) )
3 simpll 
 |-  ( ( ( ( A = C \/ A = D ) /\ ( A = C \/ B = C ) ) /\ ( ( B = D \/ A = D ) /\ ( B = D \/ B = C ) ) ) -> ( A = C \/ A = D ) )
4 pm1.4 
 |-  ( ( B = D \/ B = C ) -> ( B = C \/ B = D ) )
5 4 ad2antll 
 |-  ( ( ( ( A = C \/ A = D ) /\ ( A = C \/ B = C ) ) /\ ( ( B = D \/ A = D ) /\ ( B = D \/ B = C ) ) ) -> ( B = C \/ B = D ) )
6 3 5 jca 
 |-  ( ( ( ( A = C \/ A = D ) /\ ( A = C \/ B = C ) ) /\ ( ( B = D \/ A = D ) /\ ( B = D \/ B = C ) ) ) -> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) )
7 2 6 sylbi 
 |-  ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) -> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) )
8 1 7 syl6bi 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } -> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) ) )
9 ianor 
 |-  ( -. ( A =/= C /\ A =/= D ) <-> ( -. A =/= C \/ -. A =/= D ) )
10 nne 
 |-  ( -. A =/= C <-> A = C )
11 nne 
 |-  ( -. A =/= D <-> A = D )
12 10 11 orbi12i 
 |-  ( ( -. A =/= C \/ -. A =/= D ) <-> ( A = C \/ A = D ) )
13 9 12 bitr2i 
 |-  ( ( A = C \/ A = D ) <-> -. ( A =/= C /\ A =/= D ) )
14 ianor 
 |-  ( -. ( B =/= C /\ B =/= D ) <-> ( -. B =/= C \/ -. B =/= D ) )
15 nne 
 |-  ( -. B =/= C <-> B = C )
16 nne 
 |-  ( -. B =/= D <-> B = D )
17 15 16 orbi12i 
 |-  ( ( -. B =/= C \/ -. B =/= D ) <-> ( B = C \/ B = D ) )
18 14 17 bitr2i 
 |-  ( ( B = C \/ B = D ) <-> -. ( B =/= C /\ B =/= D ) )
19 13 18 anbi12i 
 |-  ( ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) <-> ( -. ( A =/= C /\ A =/= D ) /\ -. ( B =/= C /\ B =/= D ) ) )
20 8 19 syl6ib 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } -> ( -. ( A =/= C /\ A =/= D ) /\ -. ( B =/= C /\ B =/= D ) ) ) )
21 pm4.56 
 |-  ( ( -. ( A =/= C /\ A =/= D ) /\ -. ( B =/= C /\ B =/= D ) ) <-> -. ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) )
22 20 21 syl6ib 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } -> -. ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) ) )
23 22 necon2ad 
 |-  ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) -> { A , B } =/= { C , D } ) )