# Metamath Proof Explorer

## Theorem tpssi

Description: A 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 ${⊢}\left({A}\in {D}\wedge {B}\in {D}\wedge {C}\in {D}\right)\to \left\{{A},{B},{C}\right\}\subseteq {D}$

### Proof

Step Hyp Ref Expression
1 df-tp ${⊢}\left\{{A},{B},{C}\right\}=\left\{{A},{B}\right\}\cup \left\{{C}\right\}$
2 prssi ${⊢}\left({A}\in {D}\wedge {B}\in {D}\right)\to \left\{{A},{B}\right\}\subseteq {D}$
3 2 3adant3 ${⊢}\left({A}\in {D}\wedge {B}\in {D}\wedge {C}\in {D}\right)\to \left\{{A},{B}\right\}\subseteq {D}$
4 snssi ${⊢}{C}\in {D}\to \left\{{C}\right\}\subseteq {D}$
5 4 3ad2ant3 ${⊢}\left({A}\in {D}\wedge {B}\in {D}\wedge {C}\in {D}\right)\to \left\{{C}\right\}\subseteq {D}$
6 3 5 unssd ${⊢}\left({A}\in {D}\wedge {B}\in {D}\wedge {C}\in {D}\right)\to \left\{{A},{B}\right\}\cup \left\{{C}\right\}\subseteq {D}$
7 1 6 eqsstrid ${⊢}\left({A}\in {D}\wedge {B}\in {D}\wedge {C}\in {D}\right)\to \left\{{A},{B},{C}\right\}\subseteq {D}$