Metamath Proof Explorer

Theorem tpss

Description: An unordered triple of elements of a class is a subset of the class. (Contributed by NM, 9-Apr-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Hypotheses tpss.1 ⊢ A ∈ V
tpss.2 ⊢ B ∈ V
tpss.3 ⊢ C ∈ V
Assertion tpss ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B C ⊆ D

Proof

Step Hyp Ref Expression
1 tpss.1 ⊢ A ∈ V
2 tpss.2 ⊢ B ∈ V
3 tpss.3 ⊢ C ∈ V
4 unss ⊢ A B ⊆ D ∧ C ⊆ D ↔ A B ∪ C ⊆ D
5 df-3an ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A ∈ D ∧ B ∈ D ∧ C ∈ D
6 1 2 prss ⊢ A ∈ D ∧ B ∈ D ↔ A B ⊆ D
7 3 snss ⊢ C ∈ D ↔ C ⊆ D
8 6 7 anbi12i ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B ⊆ D ∧ C ⊆ D
9 5 8 bitri ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B ⊆ D ∧ C ⊆ D
10 df-tp ⊢ A B C = A B ∪ C
11 10 sseq1i ⊢ A B C ⊆ D ↔ A B ∪ C ⊆ D
12 4 9 11 3bitr4i ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B C ⊆ D