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

Theorem tprot 3975
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 971 . . 3  |-  ( ( x  =  A  \/  x  =  B  \/  x  =  C )  <->  ( x  =  B  \/  x  =  C  \/  x  =  A )
)
21abbii 2560 . 2  |-  { x  |  ( x  =  A  \/  x  =  B  \/  x  =  C ) }  =  { x  |  (
x  =  B  \/  x  =  C  \/  x  =  A ) }
3 dftp2 3927 . 2  |-  { A ,  B ,  C }  =  { x  |  ( x  =  A  \/  x  =  B  \/  x  =  C ) }
4 dftp2 3927 . 2  |-  { B ,  C ,  A }  =  { x  |  ( x  =  B  \/  x  =  C  \/  x  =  A ) }
52, 3, 43eqtr4i 2473 1  |-  { A ,  B ,  C }  =  { B ,  C ,  A }
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 964    = wceq 1369   {cab 2429   {ctp 3886
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-3or 966  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-un 3338  df-sn 3883  df-pr 3885  df-tp 3887
This theorem is referenced by:  tpcomb  3977  tpass  3978  tpidm13  3982  tpidm23  3983  tpnzd  4002  tpprceq3  4018  fvtp2  5931  fvtp3  5932  fvtp2g  5934  fvtp3g  5935  en3lplem2  7826  nb3graprlem2  23365  nb3grapr  23366  nb3grapr2  23367  nb3gra2nb  23368  cusgra3v  23377  f13dfv  30152  frgra3v  30599  1to3vfriswmgra  30604  en3lplem2VD  31585  dvh4dimN  35097
  Copyright terms: Public domain W3C validator