Theorem snsstp3 4786

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

This proof depends on syntax axioms:   ∪ cun 3904   ⊆ wss 3906  {csn 4591  {cpr 4593  {ctp 4595

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-tp 4596

This theorem is used by:  fr3nr  7777  rngmulr  17378  srngmulr  17389  lmodsca  17405  ipsmulr  17416  ipsip  17419  phlsca  17426  topgrptset  17441  otpsle  17456  odrngmulr  17483  odrngds  17486  prdsmulr  17536  prdsip  17538  prdsds  17541  imasds  17591  imasmulr  17596  imasip  17599  fuccofval  18043  setccofval  18163  catccofval  18185  estrccofval  18209  xpccofval  18262  mpocnfldmul  21581  cnfldds  21586  psrmulr  22144  trkgitv  28769  rlocmulval  33656  idlsrgmulr  33863  signswch  35015  algmulr  43963  clsk1indlem1  44831  rngccofvalALTV  49094  ringccofvalALTV  49128  catcofval  50065  mndtcco  50422