Theorem snsstp2 4783

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

Assertion

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

Proof of Theorem snsstp2

Step	Hyp	Ref	Expression
1		snsspr2 4781	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4131	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3946	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4594	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	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-pr 4592  df-tp 4594

This theorem is referenced by:  fr3nr  7767  rngplusg  17348  srngplusg  17359  lmodplusg  17375  ipsaddg  17386  ipsvsca  17389  phlplusg  17396  topgrpplusg  17411  otpstset  17426  odrngplusg  17453  odrngle  17456  prdsplusg  17506  prdsvsca  17508  prdsle  17510  imasplusg  17566  imasvsca  17569  imasle  17572  fuchom  18016  setchomfval  18131  catchomfval  18154  estrchomfval  18177  xpchomfval  18230  mpocnfldadd  21527  cnfldle  21533  psrplusg  22087  psrvscafval  22098  trkgdist  28715  rlocaddval  33589  idlsrgplusg  33795  algaddg  43922  clsk1indlem4  44790  rngchomfvalALTV  49052  ringchomfvalALTV  49086  cathomfval  50025  mndtchom  50382