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

Theorem prnebg 4053
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 4052 . . 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 1008 . 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 2611 . . . . . . . 8  |-  ( -.  A  =/=  C  <->  A  =  C )
6 nne 2611 . . . . . . . 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 2611 . . . . . . . 8  |-  ( -.  B  =/=  C  <->  B  =  C )
11 nne 2611 . . . . . . . 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 865 . . . . 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 2461 . . . . . . . . . 10  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
18 df-ne 2607 . . . . . . . . . . 11  |-  ( A  =/=  B  <->  -.  A  =  B )
19 pm2.24 109 . . . . . . . . . . 11  |-  ( A  =  B  ->  ( -.  A  =  B  ->  { A ,  B }  =  { C ,  D } ) )
2018, 19syl5bi 217 . . . . . . . . . 10  |-  ( A  =  B  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D }
) )
2117, 20syl 16 . . . . . . . . 9  |-  ( ( A  =  C  /\  B  =  C )  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
22 preq12 3955 . . . . . . . . . 10  |-  ( ( A  =  C  /\  B  =  D )  ->  { A ,  B }  =  { C ,  D } )
2322a1d 25 . . . . . . . . 9  |-  ( ( A  =  C  /\  B  =  D )  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
2421, 23jaoi 379 . . . . . . . 8  |-  ( ( ( A  =  C  /\  B  =  C )  \/  ( A  =  C  /\  B  =  D ) )  -> 
( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
25 preq12 3955 . . . . . . . . . . 11  |-  ( ( A  =  D  /\  B  =  C )  ->  { A ,  B }  =  { D ,  C } )
26 prcom 3952 . . . . . . . . . . 11  |-  { D ,  C }  =  { C ,  D }
2725, 26syl6eq 2490 . . . . . . . . . 10  |-  ( ( A  =  D  /\  B  =  C )  ->  { A ,  B }  =  { C ,  D } )
2827a1d 25 . . . . . . . . 9  |-  ( ( A  =  D  /\  B  =  C )  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
29 eqtr3 2461 . . . . . . . . . 10  |-  ( ( A  =  D  /\  B  =  D )  ->  A  =  B )
3029, 20syl 16 . . . . . . . . 9  |-  ( ( A  =  D  /\  B  =  D )  ->  ( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
3128, 30jaoi 379 . . . . . . . 8  |-  ( ( ( A  =  D  /\  B  =  C )  \/  ( A  =  D  /\  B  =  D ) )  -> 
( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
3224, 31jaoi 379 . . . . . . 7  |-  ( ( ( ( A  =  C  /\  B  =  C )  \/  ( A  =  C  /\  B  =  D )
)  \/  ( ( A  =  D  /\  B  =  C )  \/  ( A  =  D  /\  B  =  D ) ) )  -> 
( A  =/=  B  ->  { A ,  B }  =  { C ,  D } ) )
3332com12 31 . . . . . 6  |-  ( A  =/=  B  ->  (
( ( ( A  =  C  /\  B  =  C )  \/  ( A  =  C  /\  B  =  D )
)  \/  ( ( A  =  D  /\  B  =  C )  \/  ( A  =  D  /\  B  =  D ) ) )  ->  { A ,  B }  =  { C ,  D } ) )
34333ad2ant3 1011 . . . . 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 } ) )
3516, 34syl5bi 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 }
) )
3615, 35syl5bi 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 } ) )
3736necon1ad 2677 . 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 ) ) ) )
382, 37impbid 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 965    = wceq 1369    e. wcel 1756    =/= wne 2605   {cpr 3878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-v 2973  df-un 3332  df-sn 3877  df-pr 3879
This theorem is referenced by:  zlmodzxznm  31037
  Copyright terms: Public domain W3C validator