Theorem snsstp3 4762

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 4120	. 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2		df-tp 4573	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sseqtrri 3972	1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3888   ⊆ wss 3890  {csn 4568  {cpr 4570  {ctp 4572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-tp 4573

This theorem is referenced by:  fr3nr  7720  rngmulr  17258  srngmulr  17269  lmodsca  17285  ipsmulr  17296  ipsip  17299  phlsca  17306  topgrptset  17321  otpsle  17336  odrngmulr  17363  odrngds  17366  prdsmulr  17416  prdsip  17418  prdsds  17421  imasds  17471  imasmulr  17476  imasip  17479  fuccofval  17923  setccofval  18043  catccofval  18065  estrccofval  18089  xpccofval  18142  mpocnfldmul  21354  cnfldds  21359  cnfldmulOLD  21368  cnflddsOLD  21372  psrmulr  21934  trkgitv  28532  rlocmulval  33348  idlsrgmulr  33585  signswch  34724  algmulr  43625  clsk1indlem1  44493  rngccofvalALTV  48761  ringccofvalALTV  48795  catcofval  49718  mndtcco  50075