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

Theorem tprot 4122
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 979 . . 3  |-  ( ( x  =  A  \/  x  =  B  \/  x  =  C )  <->  ( x  =  B  \/  x  =  C  \/  x  =  A )
)
21abbii 2601 . 2  |-  { x  |  ( x  =  A  \/  x  =  B  \/  x  =  C ) }  =  { x  |  (
x  =  B  \/  x  =  C  \/  x  =  A ) }
3 dftp2 4073 . 2  |-  { A ,  B ,  C }  =  { x  |  ( x  =  A  \/  x  =  B  \/  x  =  C ) }
4 dftp2 4073 . 2  |-  { B ,  C ,  A }  =  { x  |  ( x  =  B  \/  x  =  C  \/  x  =  A ) }
52, 3, 43eqtr4i 2506 1  |-  { A ,  B ,  C }  =  { B ,  C ,  A }
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 972    = wceq 1379   {cab 2452   {ctp 4031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030  df-tp 4032
This theorem is referenced by:  tpcomb  4124  tpass  4125  tpidm13  4129  tpidm23  4130  tpnzd  4149  tpprceq3  4167  fvtp2  6109  fvtp3  6110  fvtp2g  6112  fvtp3g  6113  f13dfv  6168  en3lplem2  8032  nb3graprlem2  24156  nb3grapr  24157  nb3grapr2  24158  nb3gra2nb  24159  cusgra3v  24168  frgra3v  24706  1to3vfriswmgra  24711  en3lplem2VD  32742  dvh4dimN  36262
  Copyright terms: Public domain W3C validator