Theorem tprot 4753

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 1092	. . 3 ⊢ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴))
2	1	abbii 2802	. 2 ⊢ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)}
3		dftp2 4693	. 2 ⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)}
4		dftp2 4693	. 2 ⊢ {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)}
5	2, 3, 4	3eqtr4i 2770	1 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}

Syntax hints:   ∨ w3o 1086   = wceq 1541  {cab 2709  {ctp 4632

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-sn 4629  df-pr 4631  df-tp 4633

This theorem is referenced by:  tpcomb  4755  tpass  4756  tpidm13  4760  tpidm23  4761  tpprceq3  4807  fvtp2  7199  fvtp3  7200  fvtp2g  7202  fvtp3g  7203  f13dfv  7274  en3lplem2  9610  estrres  18095  nb3grprlem2  28893  nb3grpr  28894  nb3grpr2  28895  nb3gr2nb  28896  cplgr3v  28947  frgr3v  29783  1to3vfriswmgr  29788  dvh4dimN  40621  en3lplem2VD  43907