Theorem snsstp3 4784

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 4594	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sseqtrri 3986	1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3903   ⊆ wss 3905  {csn 4589  {cpr 4591  {ctp 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-tp 4594

This theorem is referenced by:  fr3nr  7767  rngmulr  17349  srngmulr  17360  lmodsca  17376  ipsmulr  17387  ipsip  17390  phlsca  17397  topgrptset  17412  otpsle  17427  odrngmulr  17454  odrngds  17457  prdsmulr  17507  prdsip  17509  prdsds  17512  imasds  17562  imasmulr  17567  imasip  17570  fuccofval  18014  setccofval  18134  catccofval  18156  estrccofval  18180  xpccofval  18233  mpocnfldmul  21529  cnfldds  21534  psrmulr  22092  trkgitv  28716  rlocmulval  33590  idlsrgmulr  33797  signswch  34948  algmulr  43923  clsk1indlem1  44791  rngccofvalALTV  49055  ringccofvalALTV  49089  catcofval  50026  mndtcco  50383