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.

Step	Hyp	Ref	Expression
1		3orrot 1089	. . 3 ⊢ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴))
2	1	abbii 2863	. 2 ⊢ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)}
3		dftp2 4587	. 2 ⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)}
4		dftp2 4587	. 2 ⊢ {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)}
5	2, 3, 4	3eqtr4i 2831	1 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}

Syntax hints:   ∨ w3o 1083   = wceq 1538  {cab 2776  {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 2770

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 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  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  6935  fvtp3  6936  fvtp2g  6938  fvtp3g  6939  f13dfv  7009  en3lplem2  9060  estrres  17381  nb3grprlem2  27171  nb3grpr  27172  nb3grpr2  27173  nb3gr2nb  27174  cplgr3v  27225  frgr3v  28060  1to3vfriswmgr  28065  dvh4dimN  38743  en3lplem2VD  41550