Theorem snsstp3 4774

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

Syntax hints:   ∪ cun 3899   ⊆ wss 3901  {csn 4580  {cpr 4582  {ctp 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-tp 4585

This theorem is referenced by:  fr3nr  7717  rngmulr  17221  srngmulr  17232  lmodsca  17248  ipsmulr  17259  ipsip  17262  phlsca  17269  topgrptset  17284  otpsle  17299  odrngmulr  17326  odrngds  17329  prdsmulr  17379  prdsip  17381  prdsds  17384  imasds  17434  imasmulr  17439  imasip  17442  fuccofval  17886  setccofval  18006  catccofval  18028  estrccofval  18052  xpccofval  18105  mpocnfldmul  21316  cnfldds  21321  cnfldmulOLD  21330  cnflddsOLD  21334  psrmulr  21898  trkgitv  28519  rlocmulval  33351  idlsrgmulr  33588  signswch  34718  algmulr  43428  clsk1indlem1  44296  rngccofvalALTV  48526  ringccofvalALTV  48560  catcofval  49483  mndtcco  49840