Theorem snsstp2 4760

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 4758	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4118	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3931	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4572	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3971	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3887   ⊆ wss 3889  {csn 4567  {cpr 4569  {ctp 4571

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-pr 4570  df-tp 4572

This theorem is referenced by:  fr3nr  7726  rngplusg  17263  srngplusg  17274  lmodplusg  17290  ipsaddg  17301  ipsvsca  17304  phlplusg  17311  topgrpplusg  17326  otpstset  17341  odrngplusg  17368  odrngle  17371  prdsplusg  17421  prdsvsca  17423  prdsle  17425  imasplusg  17481  imasvsca  17484  imasle  17487  fuchom  17931  setchomfval  18046  catchomfval  18069  estrchomfval  18092  xpchomfval  18145  mpocnfldadd  21357  cnfldle  21363  psrplusg  21916  psrvscafval  21927  trkgdist  28514  rlocaddval  33329  idlsrgplusg  33565  algaddg  43603  clsk1indlem4  44471  rngchomfvalALTV  48743  ringchomfvalALTV  48777  cathomfval  49702  mndtchom  50059