Theorem tpssbd

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

	Ref	Expression
Hypotheses	tpssbd.1	$$⊢\phi \to B\in V$$
	tpssbd.2	$$⊢\phi \to \left\{A,B,C\right\}\subseteq D$$
Assertion	tpssbd	$$⊢\phi \to B\in D$$

Proof

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