Theorem tpass

Description: Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Assertion	tpass	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 } ∪ { 𝐵 , 𝐶 } )

Proof

Step	Hyp	Ref	Expression
1		df-tp	⊢ { 𝐵 , 𝐶 , 𝐴 } = ( { 𝐵 , 𝐶 } ∪ { 𝐴 } )
2		tprot	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 }
3		uncom	⊢ ( { 𝐴 } ∪ { 𝐵 , 𝐶 } ) = ( { 𝐵 , 𝐶 } ∪ { 𝐴 } )
4	1 2 3	3eqtr4i	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 } ∪ { 𝐵 , 𝐶 } )