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

Theorem tprot 4645
 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 1089 . . 3 ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) ↔ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴))
21abbii 2823 . 2 {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
3 dftp2 4587 . 2 {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)}
4 dftp2 4587 . 2 {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
52, 3, 43eqtr4i 2791 1 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
 Colors of variables: wff setvar class Syntax hints:   ∨ w3o 1083   = wceq 1538  {cab 2735  {ctp 4529 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-sn 4526  df-pr 4528  df-tp 4530 This theorem is referenced by:  tpcomb  4647  tpass  4648  tpidm13  4652  tpidm23  4653  tpprceq3  4697  fvtp2  6954  fvtp3  6955  fvtp2g  6957  fvtp3g  6958  f13dfv  7028  en3lplem2  9114  estrres  17460  nb3grprlem2  27275  nb3grpr  27276  nb3grpr2  27277  nb3gr2nb  27278  cplgr3v  27329  frgr3v  28164  1to3vfriswmgr  28169  dvh4dimN  39049  en3lplem2VD  41951
 Copyright terms: Public domain W3C validator