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

Proof

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