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

Theorem tprot 4683
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 1086 . . 3 ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) ↔ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴))
21abbii 2890 . 2 {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
3 dftp2 4625 . 2 {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)}
4 dftp2 4625 . 2 {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
52, 3, 43eqtr4i 2858 1 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
Colors of variables: wff setvar class
Syntax hints:  w3o 1080   = wceq 1530  {cab 2803  {ctp 4567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-un 3944  df-sn 4564  df-pr 4566  df-tp 4568
This theorem is referenced by:  tpcomb  4685  tpass  4686  tpidm13  4690  tpidm23  4691  tpprceq3  4735  fvtp2  6957  fvtp3  6958  fvtp2g  6960  fvtp3g  6961  f13dfv  7028  en3lplem2  9068  estrres  17381  nb3grprlem2  27079  nb3grpr  27080  nb3grpr2  27081  nb3gr2nb  27082  cplgr3v  27133  frgr3v  27970  1to3vfriswmgr  27975  dvh4dimN  38452  en3lplem2VD  41045
  Copyright terms: Public domain W3C validator