Theorem tpssi 4792

Description: An unordered triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.)

Assertion

Ref	Expression
tpssi	⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)

Proof of Theorem tpssi

Step	Hyp	Ref	Expression
1		df-tp 4589	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prssi 4776	. . . 4 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ⊆ 𝐷)
3	2	3adant3 1150	. . 3 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵} ⊆ 𝐷)
4		snssi 4742	. . . 4 ⊢ (𝐶 ∈ 𝐷 → {𝐶} ⊆ 𝐷)
5	4	3ad2ant3 1153	. . 3 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐶} ⊆ 𝐷)
6	3, 5	unssd 4189	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ({𝐴, 𝐵} ∪ {𝐶}) ⊆ 𝐷)
7	1, 6	eqsstrid 3947	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2144   ⊆ wss 3896   ∪ cun 4148  {csn 4584  {cpr 4586  {ctp 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150  df-sn 4585  df-pr 4587  df-tp 4589

This theorem is used by:  sgnrn  15260  sgnclre  15264  lcmftp  16820  trgcgrg  28987  tpssd  33185  cyc3co2  33751  signstf  35245  limsupequzlem  46868  fourierdlem46  47298  fourierdlem102  47354  fourierdlem114  47366  etransclem48  47428  grtrissvtx  49178  grtrimap  49182  usgrexmpl2nb0  49265  usgrexmpl2nb3  49268