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↔ABC⊆D

Proof

Step Hyp Ref Expression
1 tpss.1 ⊢A∈V
2 tpss.2 ⊢B∈V
3 tpss.3 ⊢C∈V
4 unss ⊢AB⊆D∧C⊆D↔AB∪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↔AB⊆D
7 3 snss ⊢C∈D↔C⊆D
8 6 7 anbi12i ⊢A∈D∧B∈D∧C∈D↔AB⊆D∧C⊆D
9 5 8 bitri ⊢A∈D∧B∈D∧C∈D↔AB⊆D∧C⊆D
10 df-tp ⊢ABC=AB∪C
11 10 sseq1i ⊢ABC⊆D↔AB∪C⊆D
12 4 9 11 3bitr4i ⊢A∈D∧B∈D∧C∈D↔ABC⊆D