Theorem snsstp2 4771

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 4769	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4128	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3941	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4583	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3981	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3897   ⊆ wss 3899  {csn 4578  {cpr 4580  {ctp 4582

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-pr 4581  df-tp 4583

This theorem is referenced by:  fr3nr  7715  rngplusg  17218  srngplusg  17229  lmodplusg  17245  ipsaddg  17256  ipsvsca  17259  phlplusg  17266  topgrpplusg  17281  otpstset  17296  odrngplusg  17323  odrngle  17326  prdsplusg  17376  prdsvsca  17378  prdsle  17380  imasplusg  17436  imasvsca  17439  imasle  17442  fuchom  17886  setchomfval  18001  catchomfval  18024  estrchomfval  18047  xpchomfval  18100  mpocnfldadd  21312  cnfldle  21318  cnfldaddOLD  21327  cnfldleOLD  21331  psrplusg  21890  psrvscafval  21902  trkgdist  28467  rlocaddval  33299  idlsrgplusg  33535  algaddg  43359  clsk1indlem4  44227  rngchomfvalALTV  48455  ringchomfvalALTV  48489  cathomfval  49414  mndtchom  49771