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	$$⊢\phi \to C\in V$$
	tpsscd.2	$$⊢\phi \to \left\{A,B,C\right\}\subseteq D$$
Assertion	tpsscd	$$⊢\phi \to C\in D$$

Proof

Step	Hyp	Ref	Expression
1		tpsscd.1	$$⊢\phi \to C\in V$$
2		tpsscd.2	$$⊢\phi \to \left\{A,B,C\right\}\subseteq D$$
3		tprot	$$⊢\left\{A,B,C\right\}=\left\{B,C,A\right\}$$
4		tprot	$$⊢\left\{B,C,A\right\}=\left\{C,A,B\right\}$$
5	3 4	eqtri	$$⊢\left\{A,B,C\right\}=\left\{C,A,B\right\}$$
6	5 2	eqsstrrid	$$⊢\phi \to \left\{C,A,B\right\}\subseteq D$$
7	1 6	tpssad	$$⊢\phi \to C\in D$$