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 𝐴 ∈ V
tpss.2 𝐵 ∈ V
tpss.3 𝐶 ∈ V
Assertion tpss ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) ↔ { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )

Proof

Step Hyp Ref Expression
1 tpss.1 𝐴 ∈ V
2 tpss.2 𝐵 ∈ V
3 tpss.3 𝐶 ∈ V
4 unss ( ( { 𝐴 , 𝐵 } ⊆ 𝐷 ∧ { 𝐶 } ⊆ 𝐷 ) ↔ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ⊆ 𝐷 )
5 df-3an ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) ↔ ( ( 𝐴𝐷𝐵𝐷 ) ∧ 𝐶𝐷 ) )
6 1 2 prss ( ( 𝐴𝐷𝐵𝐷 ) ↔ { 𝐴 , 𝐵 } ⊆ 𝐷 )
7 3 snss ( 𝐶𝐷 ↔ { 𝐶 } ⊆ 𝐷 )
8 6 7 anbi12i ( ( ( 𝐴𝐷𝐵𝐷 ) ∧ 𝐶𝐷 ) ↔ ( { 𝐴 , 𝐵 } ⊆ 𝐷 ∧ { 𝐶 } ⊆ 𝐷 ) )
9 5 8 bitri ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) ↔ ( { 𝐴 , 𝐵 } ⊆ 𝐷 ∧ { 𝐶 } ⊆ 𝐷 ) )
10 df-tp { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
11 10 sseq1i ( { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 ↔ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ⊆ 𝐷 )
12 4 9 11 3bitr4i ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) ↔ { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )