Theorem tprot

Description: Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011)

	Ref	Expression
Assertion	tprot	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 }

Proof

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