Theorem tpssi

Description: An unordered triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018)

	Ref	Expression
Assertion	tpssi	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		df-tp	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
2		prssi	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 , 𝐵 } ⊆ 𝐷 )
3	2	3adant3	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → { 𝐴 , 𝐵 } ⊆ 𝐷 )
4		snssi	⊢ ( 𝐶 ∈ 𝐷 → { 𝐶 } ⊆ 𝐷 )
5	4	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → { 𝐶 } ⊆ 𝐷 )
6	3 5	unssd	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ⊆ 𝐷 )
7	1 6	eqsstrid	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )