Theorem snsstp3 4785

Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)

Assertion

Ref	Expression
snsstp3	⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}

Proof of Theorem snsstp3

Step	Hyp	Ref	Expression
1		ssun2 4145	. 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2		df-tp 4597	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sseqtrri 3999	1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3915   ⊆ wss 3917  {csn 4592  {cpr 4594  {ctp 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-tp 4597

This theorem is referenced by:  fr3nr  7751  rngmulr  17271  srngmulr  17282  lmodsca  17298  ipsmulr  17309  ipsip  17312  phlsca  17319  topgrptset  17334  otpsle  17349  odrngmulr  17376  odrngds  17379  prdsmulr  17429  prdsip  17431  prdsds  17434  imasds  17483  imasmulr  17488  imasip  17491  fuccofval  17931  setccofval  18051  catccofval  18073  estrccofval  18097  xpccofval  18150  mpocnfldmul  21278  cnfldds  21283  cnfldmulOLD  21292  cnflddsOLD  21296  psrmulr  21858  trkgitv  28381  rlocmulval  33227  idlsrgmulr  33485  signswch  34559  algmulr  43172  clsk1indlem1  44041  rngccofvalALTV  48262  ringccofvalALTV  48296  catcofval  49221  mndtcco  49578