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

Theorem tprot 4746
Description: Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
Assertion
Ref Expression
tprot {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}

Proof of Theorem tprot
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 3orrot 1092 . . 3 ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) ↔ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴))
21abbii 2801 . 2 {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
3 dftp2 4686 . 2 {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)}
4 dftp2 4686 . 2 {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
52, 3, 43eqtr4i 2769 1 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
Colors of variables: wff setvar class
Syntax hints:  w3o 1086   = wceq 1541  {cab 2708  {ctp 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3949  df-sn 4623  df-pr 4625  df-tp 4627
This theorem is referenced by:  tpcomb  4748  tpass  4749  tpidm13  4753  tpidm23  4754  tpprceq3  4800  fvtp2  7181  fvtp3  7182  fvtp2g  7184  fvtp3g  7185  f13dfv  7256  en3lplem2  9590  estrres  18073  nb3grprlem2  28503  nb3grpr  28504  nb3grpr2  28505  nb3gr2nb  28506  cplgr3v  28557  frgr3v  29393  1to3vfriswmgr  29398  dvh4dimN  40123  en3lplem2VD  43376
  Copyright terms: Public domain W3C validator