Theorem tpssi 4798

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 4593	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prssi 4782	. . . 4 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ⊆ 𝐷)
3	2	3adant3 1150	. . 3 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵} ⊆ 𝐷)
4		snssi 4748	. . . 4 ⊢ (𝐶 ∈ 𝐷 → {𝐶} ⊆ 𝐷)
5	4	3ad2ant3 1153	. . 3 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐶} ⊆ 𝐷)
6	3, 5	unssd 4193	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ({𝐴, 𝐵} ∪ {𝐶}) ⊆ 𝐷)
7	1, 6	eqsstrid 3951	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2147   ⊆ wss 3900   ∪ cun 4152  {csn 4588  {cpr 4590  {ctp 4592

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-tp 4593

This theorem is used by:  sgnrn  15294  sgnclre  15298  lcmftp  16855  trgcgrg  29035  tpssd  33232  cyc3co2  33800  signstf  35306  limsupequzlem  47005  fourierdlem46  47435  fourierdlem102  47491  fourierdlem114  47503  etransclem48  47565  grtrissvtx  49315  grtrimap  49319  usgrexmpl2nb0  49402  usgrexmpl2nb3  49405