Theorem tpssi

Description: An unordered triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018)

	Ref	Expression
Assertion	tpssi	|- ( ( A e. D /\ B e. D /\ C e. D ) -> { A , B , C } C_ D )

Proof

Step	Hyp	Ref	Expression
1		df-tp	|- { A , B , C } = ( { A , B } u. { C } )
2		prssi	|- ( ( A e. D /\ B e. D ) -> { A , B } C_ D )
3	2	3adant3	|- ( ( A e. D /\ B e. D /\ C e. D ) -> { A , B } C_ D )
4		snssi	|- ( C e. D -> { C } C_ D )
5	4	3ad2ant3	|- ( ( A e. D /\ B e. D /\ C e. D ) -> { C } C_ D )
6	3 5	unssd	|- ( ( A e. D /\ B e. D /\ C e. D ) -> ( { A , B } u. { C } ) C_ D )
7	1 6	eqsstrid	|- ( ( A e. D /\ B e. D /\ C e. D ) -> { A , B , C } C_ D )