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	|- ( ph -> B e. V )
	tpssbd.2	|- ( ph -> { A , B , C } C_ D )
Assertion	tpssbd	|- ( ph -> B e. D )

Proof

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