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

Theorem tprot 4089
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 988 . . 3  |-  ( ( x  =  A  \/  x  =  B  \/  x  =  C )  <->  ( x  =  B  \/  x  =  C  \/  x  =  A )
)
21abbii 2554 . 2  |-  { x  |  ( x  =  A  \/  x  =  B  \/  x  =  C ) }  =  { x  |  (
x  =  B  \/  x  =  C  \/  x  =  A ) }
3 dftp2 4040 . 2  |-  { A ,  B ,  C }  =  { x  |  ( x  =  A  \/  x  =  B  \/  x  =  C ) }
4 dftp2 4040 . 2  |-  { B ,  C ,  A }  =  { x  |  ( x  =  B  \/  x  =  C  \/  x  =  A ) }
52, 3, 43eqtr4i 2459 1  |-  { A ,  B ,  C }  =  { B ,  C ,  A }
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 981    = wceq 1437   {cab 2405   {ctp 3997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-un 3438  df-sn 3994  df-pr 3996  df-tp 3998
This theorem is referenced by:  tpcomb  4091  tpass  4092  tpidm13  4096  tpidm23  4097  tpnzd  4116  tpprceq3  4134  fvtp2  6118  fvtp3  6119  fvtp2g  6121  fvtp3g  6122  f13dfv  6179  en3lplem2  8111  estrres  15968  nb3graprlem2  25051  nb3grapr  25052  nb3grapr2  25053  nb3gra2nb  25054  cusgra3v  25063  frgra3v  25601  1to3vfriswmgra  25606  dvh4dimN  34753  en3lplem2VD  36913
  Copyright terms: Public domain W3C validator