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 ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )

Proof

Step Hyp Ref Expression
1 df-tp { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
2 prssi ( ( 𝐴𝐷𝐵𝐷 ) → { 𝐴 , 𝐵 } ⊆ 𝐷 )
3 2 3adant3 ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) → { 𝐴 , 𝐵 } ⊆ 𝐷 )
4 snssi ( 𝐶𝐷 → { 𝐶 } ⊆ 𝐷 )
5 4 3ad2ant3 ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) → { 𝐶 } ⊆ 𝐷 )
6 3 5 unssd ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) → ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ⊆ 𝐷 )
7 1 6 eqsstrid ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )