Theorem snsstp2 4773

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 4771	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4130	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3943	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4585	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3983	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3899   ⊆ wss 3901  {csn 4580  {cpr 4582  {ctp 4584

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-pr 4583  df-tp 4585

This theorem is referenced by:  fr3nr  7717  rngplusg  17220  srngplusg  17231  lmodplusg  17247  ipsaddg  17258  ipsvsca  17261  phlplusg  17268  topgrpplusg  17283  otpstset  17298  odrngplusg  17325  odrngle  17328  prdsplusg  17378  prdsvsca  17380  prdsle  17382  imasplusg  17438  imasvsca  17441  imasle  17444  fuchom  17888  setchomfval  18003  catchomfval  18026  estrchomfval  18049  xpchomfval  18102  mpocnfldadd  21314  cnfldle  21320  cnfldaddOLD  21329  cnfldleOLD  21333  psrplusg  21892  psrvscafval  21904  trkgdist  28518  rlocaddval  33350  idlsrgplusg  33586  algaddg  43427  clsk1indlem4  44295  rngchomfvalALTV  48523  ringchomfvalALTV  48557  cathomfval  49482  mndtchom  49839