MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prnebg Structured version   Unicode version

Theorem prnebg 4214
Description: A (proper) pair is not equal to another (maybe inproper) 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.)
Assertion
Ref Expression
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 of Theorem prnebg
StepHypRef Expression
1 prneimg 4213 . . 3  |-  ( ( ( A  e.  U  /\  B  e.  V
)  /\  ( C  e.  X  /\  D  e.  Y ) )  -> 
( ( ( A  =/=  C  /\  A  =/=  D )  \/  ( B  =/=  C  /\  B  =/=  D ) )  ->  { A ,  B }  =/=  { C ,  D } ) )
213adant3 1016 . 2  |-  ( ( ( 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 490 . . . . 5  |-  ( -.  ( ( A  =/= 
C  /\  A  =/=  D )  \/  ( B  =/=  C  /\  B  =/=  D ) )  <->  ( -.  ( A  =/=  C  /\  A  =/=  D
)  /\  -.  ( B  =/=  C  /\  B  =/=  D ) ) )
4 ianor 488 . . . . . . 7  |-  ( -.  ( A  =/=  C  /\  A  =/=  D
)  <->  ( -.  A  =/=  C  \/  -.  A  =/=  D ) )
5 nne 2658 . . . . . . . 8  |-  ( -.  A  =/=  C  <->  A  =  C )
6 nne 2658 . . . . . . . 8  |-  ( -.  A  =/=  D  <->  A  =  D )
75, 6orbi12i 521 . . . . . . 7  |-  ( ( -.  A  =/=  C  \/  -.  A  =/=  D
)  <->  ( A  =  C  \/  A  =  D ) )
84, 7bitri 249 . . . . . 6  |-  ( -.  ( A  =/=  C  /\  A  =/=  D
)  <->  ( A  =  C  \/  A  =  D ) )
9 ianor 488 . . . . . . 7  |-  ( -.  ( B  =/=  C  /\  B  =/=  D
)  <->  ( -.  B  =/=  C  \/  -.  B  =/=  D ) )
10 nne 2658 . . . . . . . 8  |-  ( -.  B  =/=  C  <->  B  =  C )
11 nne 2658 . . . . . . . 8  |-  ( -.  B  =/=  D  <->  B  =  D )
1210, 11orbi12i 521 . . . . . . 7  |-  ( ( -.  B  =/=  C  \/  -.  B  =/=  D
)  <->  ( B  =  C  \/  B  =  D ) )
139, 12bitri 249 . . . . . 6  |-  ( -.  ( B  =/=  C  /\  B  =/=  D
)  <->  ( B  =  C  \/  B  =  D ) )
148, 13anbi12i 697 . . . . 5  |-  ( ( -.  ( A  =/= 
C  /\  A  =/=  D )  /\  -.  ( B  =/=  C  /\  B  =/=  D ) )  <->  ( ( A  =  C  \/  A  =  D )  /\  ( B  =  C  \/  B  =  D ) ) )
153, 14bitri 249 . . . 4  |-  ( -.  ( ( A  =/= 
C  /\  A  =/=  D )  \/  ( B  =/=  C  /\  B  =/=  D ) )  <->  ( ( A  =  C  \/  A  =  D )  /\  ( B  =  C  \/  B  =  D ) ) )
16 anddi 870 . . . . 5  |-  ( ( ( 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 2485 . . . . . . . . . 10  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
18 eqneqall 2664 . . . . . . . . . 10  |-  ( A  =  B  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D }
) )
1917, 18syl 16 . . . . . . . . 9  |-  ( ( A  =  C  /\  B  =  C )  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
20 preq12 4113 . . . . . . . . . 10  |-  ( ( A  =  C  /\  B  =  D )  ->  { A ,  B }  =  { C ,  D } )
2120a1d 25 . . . . . . . . 9  |-  ( ( A  =  C  /\  B  =  D )  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
2219, 21jaoi 379 . . . . . . . 8  |-  ( ( ( A  =  C  /\  B  =  C )  \/  ( A  =  C  /\  B  =  D ) )  -> 
( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
23 preq12 4113 . . . . . . . . . . 11  |-  ( ( A  =  D  /\  B  =  C )  ->  { A ,  B }  =  { D ,  C } )
24 prcom 4110 . . . . . . . . . . 11  |-  { D ,  C }  =  { C ,  D }
2523, 24syl6eq 2514 . . . . . . . . . 10  |-  ( ( A  =  D  /\  B  =  C )  ->  { A ,  B }  =  { C ,  D } )
2625a1d 25 . . . . . . . . 9  |-  ( ( A  =  D  /\  B  =  C )  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
27 eqtr3 2485 . . . . . . . . . 10  |-  ( ( A  =  D  /\  B  =  D )  ->  A  =  B )
2827, 18syl 16 . . . . . . . . 9  |-  ( ( A  =  D  /\  B  =  D )  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
2926, 28jaoi 379 . . . . . . . 8  |-  ( ( ( A  =  D  /\  B  =  C )  \/  ( A  =  D  /\  B  =  D ) )  -> 
( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
3022, 29jaoi 379 . . . . . . 7  |-  ( ( ( ( A  =  C  /\  B  =  C )  \/  ( A  =  C  /\  B  =  D )
)  \/  ( ( A  =  D  /\  B  =  C )  \/  ( A  =  D  /\  B  =  D ) ) )  -> 
( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
3130com12 31 . . . . . 6  |-  ( A  =/=  B  ->  (
( ( ( A  =  C  /\  B  =  C )  \/  ( A  =  C  /\  B  =  D )
)  \/  ( ( A  =  D  /\  B  =  C )  \/  ( A  =  D  /\  B  =  D ) ) )  ->  { A ,  B }  =  { C ,  D } ) )
32313ad2ant3 1019 . . . . 5  |-  ( ( ( 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 } ) )
3316, 32syl5bi 217 . . . 4  |-  ( ( ( 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 }
) )
3415, 33syl5bi 217 . . 3  |-  ( ( ( 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 } ) )
3534necon1ad 2673 . 2  |-  ( ( ( 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 ) ) ) )
362, 35impbid 191 1  |-  ( ( ( 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 }
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 973    = wceq 1395    e. wcel 1819    =/= wne 2652   {cpr 4034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-un 3476  df-sn 4033  df-pr 4035
This theorem is referenced by:  zlmodzxznm  33200
  Copyright terms: Public domain W3C validator