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

Theorem tprot 4070
Description: Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
Assertion
Ref Expression
tprot  |-  { A ,  B ,  C }  =  { B ,  C ,  A }

Proof of Theorem tprot
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 3orrot 992 . . 3  |-  ( ( x  =  A  \/  x  =  B  \/  x  =  C )  <->  ( x  =  B  \/  x  =  C  \/  x  =  A )
)
21abbii 2569 . 2  |-  { x  |  ( x  =  A  \/  x  =  B  \/  x  =  C ) }  =  { x  |  (
x  =  B  \/  x  =  C  \/  x  =  A ) }
3 dftp2 4020 . 2  |-  { A ,  B ,  C }  =  { x  |  ( x  =  A  \/  x  =  B  \/  x  =  C ) }
4 dftp2 4020 . 2  |-  { B ,  C ,  A }  =  { x  |  ( x  =  B  \/  x  =  C  \/  x  =  A ) }
52, 3, 43eqtr4i 2485 1  |-  { A ,  B ,  C }  =  { B ,  C ,  A }
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 985    = wceq 1446   {cab 2439   {ctp 3974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-un 3411  df-sn 3971  df-pr 3973  df-tp 3975
This theorem is referenced by:  tpcomb  4072  tpass  4073  tpidm13  4077  tpidm23  4078  tpnzd  4097  tpprceq3  4115  fvtp2  6117  fvtp3  6118  fvtp2g  6120  fvtp3g  6121  f13dfv  6178  en3lplem2  8125  estrres  16036  nb3graprlem2  25192  nb3grapr  25193  nb3grapr2  25194  nb3gra2nb  25195  cusgra3v  25204  frgra3v  25742  1to3vfriswmgra  25747  dvh4dimN  35027  en3lplem2VD  37250  nb3grprlem2  39465  nb3grpr  39466  nb3grpr2  39467  nb3gr2nb  39468  cplgr3v  39512
  Copyright terms: Public domain W3C validator