Theorem tprot 4749

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 2809	. 2 ⊢ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)}
3		dftp2 4691	. 2 ⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)}
4		dftp2 4691	. 2 ⊢ {𝐵, 𝐶, 𝐴} = {𝑥 ∣ (𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ∨ 𝑥 = 𝐴)}
5	2, 3, 4	3eqtr4i 2775	1 ⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}

Syntax hints:   ∨ w3o 1086   = wceq 1540  {cab 2714  {ctp 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629  df-tp 4631

This theorem is referenced by:  tpcomb  4751  tpass  4752  tpidm13  4756  tpidm23  4757  tpprceq3  4804  fvtp2  7216  fvtp3  7217  fvtp2g  7219  fvtp3g  7220  f13dfv  7294  en3lplem2  9653  estrres  18184  nb3grprlem2  29398  nb3grpr  29399  nb3grpr2  29400  nb3gr2nb  29401  cplgr3v  29452  frgr3v  30294  1to3vfriswmgr  30299  dvh4dimN  41449  en3lplem2VD  44864