Theorem tpssd

Description: Deduction version of tpssi : An unordered triple of elements of a class is a subset of that class. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Hypotheses	tpssd.1	|- ( ph -> A e. D )
	tpssd.2	|- ( ph -> B e. D )
	tpssd.3	|- ( ph -> C e. D )
Assertion	tpssd	|- ( ph -> { A , B , C } C_ D )

Proof

Step	Hyp	Ref	Expression
1		tpssd.1	|- ( ph -> A e. D )
2		tpssd.2	|- ( ph -> B e. D )
3		tpssd.3	|- ( ph -> C e. D )
4		tpssi	|- ( ( A e. D /\ B e. D /\ C e. D ) -> { A , B , C } C_ D )
5	1 2 3 4	syl3anc	|- ( ph -> { A , B , C } C_ D )