Theorem tprot 4701

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 1091	. . 3 ⊢ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴))
2	1	abbii 2798	. 2 ⊢ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)}
3		dftp2 4643	. 2 ⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)}
4		dftp2 4643	. 2 ⊢ {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)}
5	2, 3, 4	3eqtr4i 2764	1 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}

Syntax hints:   ∨ w3o 1085   = wceq 1541  {cab 2709  {ctp 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4576  df-pr 4578  df-tp 4580

This theorem is referenced by:  tpcomb  4703  tpass  4704  tpidm13  4708  tpidm23  4709  tpprceq3  4755  fvtp2  7136  fvtp3  7137  fvtp2g  7139  fvtp3g  7140  f13dfv  7214  en3lplem2  9509  estrres  18051  ex-chn2  18550  nb3grprlem2  29366  nb3grpr  29367  nb3grpr2  29368  nb3gr2nb  29369  cplgr3v  29420  frgr3v  30262  1to3vfriswmgr  30267  tpssbd  32527  tpsscd  32528  dvh4dimN  41552  en3lplem2VD  44941