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 D B D C D A B C D

Proof

Step Hyp Ref Expression
1 df-tp A B C = A B C
2 prssi A D B D A B D
3 2 3adant3 A D B D C D A B D
4 snssi C D C D
5 4 3ad2ant3 A D B D C D C D
6 3 5 unssd A D B D C D A B C D
7 1 6 eqsstrid A D B D C D A B C D