Theorem snsstp2 4781

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 4779	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4141	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3956	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4594	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3996	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3912   ⊆ wss 3914  {csn 4589  {cpr 4591  {ctp 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-pr 4592  df-tp 4594

This theorem is referenced by:  fr3nr  7748  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  17480  imasvsca  17483  imasle  17486  fuchom  17926  setchomfval  18041  catchomfval  18064  estrchomfval  18087  xpchomfval  18140  mpocnfldadd  21269  cnfldle  21275  cnfldaddOLD  21284  cnfldleOLD  21288  psrplusg  21845  psrvscafval  21857  trkgdist  28373  rlocaddval  33219  idlsrgplusg  33476  algaddg  43164  clsk1indlem4  44033  rngchomfvalALTV  48255  ringchomfvalALTV  48289  cathomfval  49216  mndtchom  49573