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 e. D /\ B e. D /\ C e. D ) -> { A , B , C } C_ D )

Proof

Step Hyp Ref Expression
1 df-tp
 |-  { A , B , C } = ( { A , B } u. { C } )
2 prssi
 |-  ( ( A e. D /\ B e. D ) -> { A , B } C_ D )
3 2 3adant3
 |-  ( ( A e. D /\ B e. D /\ C e. D ) -> { A , B } C_ D )
4 snssi
 |-  ( C e. D -> { C } C_ D )
5 4 3ad2ant3
 |-  ( ( A e. D /\ B e. D /\ C e. D ) -> { C } C_ D )
6 3 5 unssd
 |-  ( ( A e. D /\ B e. D /\ C e. D ) -> ( { A , B } u. { C } ) C_ D )
7 1 6 eqsstrid
 |-  ( ( A e. D /\ B e. D /\ C e. D ) -> { A , B , C } C_ D )