Theorem snsstp2 4761

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 4759	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4119	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3932	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4573	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	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-pr 4571  df-tp 4573

This theorem is referenced by:  fr3nr  7720  rngplusg  17257  srngplusg  17268  lmodplusg  17284  ipsaddg  17295  ipsvsca  17298  phlplusg  17305  topgrpplusg  17320  otpstset  17335  odrngplusg  17362  odrngle  17365  prdsplusg  17415  prdsvsca  17417  prdsle  17419  imasplusg  17475  imasvsca  17478  imasle  17481  fuchom  17925  setchomfval  18040  catchomfval  18063  estrchomfval  18086  xpchomfval  18139  mpocnfldadd  21352  cnfldle  21358  cnfldaddOLD  21367  cnfldleOLD  21371  psrplusg  21929  psrvscafval  21940  trkgdist  28531  rlocaddval  33347  idlsrgplusg  33583  algaddg  43624  clsk1indlem4  44492  rngchomfvalALTV  48758  ringchomfvalALTV  48792  cathomfval  49717  mndtchom  50074