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

Theorem tprot 4441
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 1112 . . 3 ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) ↔ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴))
21abbii 2882 . 2 {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
3 dftp2 4389 . 2 {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶)}
4 dftp2 4389 . 2 {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶𝑥 = 𝐴)}
52, 3, 43eqtr4i 2797 1 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
Colors of variables: wff setvar class
Syntax hints:  w3o 1106   = wceq 1652  {cab 2751  {ctp 4340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3739  df-sn 4337  df-pr 4339  df-tp 4341
This theorem is referenced by:  tpcomb  4443  tpass  4444  tpidm13  4448  tpidm23  4449  tpnzd  4469  tpprceq3  4491  fvtp2  6656  fvtp3  6657  fvtp2g  6659  fvtp3g  6660  f13dfv  6724  en3lplem2  8725  estrresOLD  17047  estrres  17048  nb3grprlem2  26565  nb3grpr  26566  nb3grpr2  26567  nb3gr2nb  26568  cplgr3v  26625  frgr3v  27558  1to3vfriswmgr  27563  dvh4dimN  37406  en3lplem2VD  39735
  Copyright terms: Public domain W3C validator