This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. _V
tpss.2 
|- B e. _V
tpss.3 
|- C e. _V
Assertion tpss 
|- ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D )

Proof

Step Hyp Ref Expression
1 tpss.1 
 |-  A e. _V
2 tpss.2 
 |-  B e. _V
3 tpss.3 
 |-  C e. _V
4 unss 
 |-  ( ( { A , B } C_ D /\ { C } C_ D ) <-> ( { A , B } u. { C } ) C_ D )
5 df-3an 
 |-  ( ( A e. D /\ B e. D /\ C e. D ) <-> ( ( A e. D /\ B e. D ) /\ C e. D ) )
6 1 2 prss 
 |-  ( ( A e. D /\ B e. D ) <-> { A , B } C_ D )
7 3 snss 
 |-  ( C e. D <-> { C } C_ D )
8 6 7 anbi12i 
 |-  ( ( ( A e. D /\ B e. D ) /\ C e. D ) <-> ( { A , B } C_ D /\ { C } C_ D ) )
9 5 8 bitri 
 |-  ( ( A e. D /\ B e. D /\ C e. D ) <-> ( { A , B } C_ D /\ { C } C_ D ) )
10 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
11 10 sseq1i 
 |-  ( { A , B , C } C_ D <-> ( { A , B } u. { C } ) C_ D )
12 4 9 11 3bitr4i 
 |-  ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D )