Metamath Proof Explorer

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 ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D → A B C ⊆ D

Proof

Step Hyp Ref Expression
1 df-tp ⊢ A B C = A B ∪ C
2 prssi ⊢ A ∈ D ∧ B ∈ D → A B ⊆ D
3 2 3adant3 ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D → A B ⊆ D
4 snssi ⊢ C ∈ D → C ⊆ D
5 4 3ad2ant3 ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D → C ⊆ D
6 3 5 unssd ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D → A B ∪ C ⊆ D
7 1 6 eqsstrid ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D → A B C ⊆ D