Theorem tpsscd

Description: If an ordered triple is a subset of a class, the third element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		tpsscd.1	|- ( ph -> C e. V )
2		tpsscd.2	|- ( ph -> { A , B , C } C_ D )
3		tprot	|- { A , B , C } = { B , C , A }
4		tprot	|- { B , C , A } = { C , A , B }
5	3 4	eqtri	|- { A , B , C } = { C , A , B }
6	5 2	eqsstrrid	|- ( ph -> { C , A , B } C_ D )
7	1 6	tpssad	|- ( ph -> C e. D )