Theorem tprot

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

	Ref	Expression
Assertion	tprot	$$⊢\left\{A,B,C\right\}=\left\{B,C,A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		3orrot	$$⊢\left(x=A\vee x=B\vee x=C\right)\leftrightarrow \left(x=B\vee x=C\vee x=A\right)$$
2	1	abbii	$$⊢\left\{x|\left(x=A\vee x=B\vee x=C\right)\right\}=\left\{x|\left(x=B\vee x=C\vee x=A\right)\right\}$$
3		dftp2	$$⊢\left\{A,B,C\right\}=\left\{x|\left(x=A\vee x=B\vee x=C\right)\right\}$$
4		dftp2	$$⊢\left\{B,C,A\right\}=\left\{x|\left(x=B\vee x=C\vee x=A\right)\right\}$$
5	2 3 4	3eqtr4i	$$⊢\left\{A,B,C\right\}=\left\{B,C,A\right\}$$