Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pr1eqbg Structured version   Unicode version

Theorem pr1eqbg 32690
Description: A (proper) pair is equal to another (maybe inproper) pair containing one element of the first pair if and only if the other element of the first pair is contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
Assertion
Ref Expression
pr1eqbg  |-  ( ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X
)  /\  A  =/=  B )  ->  ( A  =  C  <->  { A ,  B }  =  { B ,  C } ) )

Proof of Theorem pr1eqbg
StepHypRef Expression
1 eqid 2454 . . . . 5  |-  B  =  B
21biantru 503 . . . 4  |-  ( A  =  C  <->  ( A  =  C  /\  B  =  B ) )
32orbi2i 517 . . 3  |-  ( ( ( A  =  B  /\  B  =  C )  \/  A  =  C )  <->  ( ( A  =  B  /\  B  =  C )  \/  ( A  =  C  /\  B  =  B ) ) )
43a1i 11 . 2  |-  ( ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X
)  /\  A  =/=  B )  ->  ( (
( A  =  B  /\  B  =  C )  \/  A  =  C )  <->  ( ( A  =  B  /\  B  =  C )  \/  ( A  =  C  /\  B  =  B ) ) ) )
5 df-ne 2651 . . . . . 6  |-  ( A  =/=  B  <->  -.  A  =  B )
65biimpi 194 . . . . 5  |-  ( A  =/=  B  ->  -.  A  =  B )
76adantl 464 . . . 4  |-  ( ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X
)  /\  A  =/=  B )  ->  -.  A  =  B )
87intnanrd 915 . . 3  |-  ( ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X
)  /\  A  =/=  B )  ->  -.  ( A  =  B  /\  B  =  C )
)
9 biorf 403 . . 3  |-  ( -.  ( A  =  B  /\  B  =  C )  ->  ( A  =  C  <->  ( ( A  =  B  /\  B  =  C )  \/  A  =  C ) ) )
108, 9syl 16 . 2  |-  ( ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X
)  /\  A  =/=  B )  ->  ( A  =  C  <->  ( ( A  =  B  /\  B  =  C )  \/  A  =  C ) ) )
11 3simpa 991 . . . . 5  |-  ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X )  ->  ( A  e.  U  /\  B  e.  V
) )
12 3simpc 993 . . . . 5  |-  ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X )  ->  ( B  e.  V  /\  C  e.  X
) )
1311, 12jca 530 . . . 4  |-  ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X )  ->  ( ( A  e.  U  /\  B  e.  V )  /\  ( B  e.  V  /\  C  e.  X )
) )
1413adantr 463 . . 3  |-  ( ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X
)  /\  A  =/=  B )  ->  ( ( A  e.  U  /\  B  e.  V )  /\  ( B  e.  V  /\  C  e.  X
) ) )
15 preq12bg 4195 . . 3  |-  ( ( ( A  e.  U  /\  B  e.  V
)  /\  ( B  e.  V  /\  C  e.  X ) )  -> 
( { A ,  B }  =  { B ,  C }  <->  ( ( A  =  B  /\  B  =  C )  \/  ( A  =  C  /\  B  =  B ) ) ) )
1614, 15syl 16 . 2  |-  ( ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X
)  /\  A  =/=  B )  ->  ( { A ,  B }  =  { B ,  C } 
<->  ( ( A  =  B  /\  B  =  C )  \/  ( A  =  C  /\  B  =  B )
) ) )
174, 10, 163bitr4d 285 1  |-  ( ( ( A  e.  U  /\  B  e.  V  /\  C  e.  X
)  /\  A  =/=  B )  ->  ( A  =  C  <->  { A ,  B }  =  { B ,  C } ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823    =/= wne 2649   {cpr 4018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-un 3466  df-sn 4017  df-pr 4019
This theorem is referenced by:  pr1nebg  32691
  Copyright terms: Public domain W3C validator