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	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	tpssbd.2	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )
Assertion	tpssbd	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		tpssbd.1	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2		tpssbd.2	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )
3		tprot	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 }
4	3 2	eqsstrrid	⊢ ( 𝜑 → { 𝐵 , 𝐶 , 𝐴 } ⊆ 𝐷 )
5	1 4	tpssad	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )