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

Theorem tprot 4749
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 2809 . 2 {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
3 dftp2 4691 . 2 {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)}
4 dftp2 4691 . 2 {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
52, 3, 43eqtr4i 2775 1 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
Colors of variables: wff setvar class
Syntax hints:  w3o 1086   = wceq 1540  {cab 2714  {ctp 4630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629  df-tp 4631
This theorem is referenced by:  tpcomb  4751  tpass  4752  tpidm13  4756  tpidm23  4757  tpprceq3  4804  fvtp2  7216  fvtp3  7217  fvtp2g  7219  fvtp3g  7220  f13dfv  7294  en3lplem2  9653  estrres  18184  nb3grprlem2  29398  nb3grpr  29399  nb3grpr2  29400  nb3gr2nb  29401  cplgr3v  29452  frgr3v  30294  1to3vfriswmgr  30299  dvh4dimN  41449  en3lplem2VD  44864
  Copyright terms: Public domain W3C validator