Theorem snsstp2 4766

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 4764	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4125	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3939	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4578	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3979	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3895   ⊆ wss 3897  {csn 4573  {cpr 4575  {ctp 4577

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914  df-pr 4576  df-tp 4578

This theorem is referenced by:  fr3nr  7705  rngplusg  17204  srngplusg  17215  lmodplusg  17231  ipsaddg  17242  ipsvsca  17245  phlplusg  17252  topgrpplusg  17267  otpstset  17282  odrngplusg  17309  odrngle  17312  prdsplusg  17362  prdsvsca  17364  prdsle  17366  imasplusg  17421  imasvsca  17424  imasle  17427  fuchom  17871  setchomfval  17986  catchomfval  18009  estrchomfval  18032  xpchomfval  18085  mpocnfldadd  21296  cnfldle  21302  cnfldaddOLD  21311  cnfldleOLD  21315  psrplusg  21873  psrvscafval  21885  trkgdist  28424  rlocaddval  33235  idlsrgplusg  33470  algaddg  43278  clsk1indlem4  44147  rngchomfvalALTV  48377  ringchomfvalALTV  48411  cathomfval  49338  mndtchom  49695