Theorem tprot

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

	Ref	Expression
Assertion	tprot	|- { A , B , C } = { B , C , A }

Proof

Step	Hyp	Ref	Expression
1		3orrot	|- ( ( x = A \/ x = B \/ x = C ) <-> ( x = B \/ x = C \/ x = A ) )
2	1	abbii	|- { x | ( x = A \/ x = B \/ x = C ) } = { x | ( x = B \/ x = C \/ x = A ) }
3		dftp2	|- { A , B , C } = { x | ( x = A \/ x = B \/ x = C ) }
4		dftp2	|- { B , C , A } = { x | ( x = B \/ x = C \/ x = A ) }
5	2 3 4	3eqtr4i	|- { A , B , C } = { B , C , A }