Theorem snsstp2 4777

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 4775	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4137	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3953	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4590	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3993	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3909   ⊆ wss 3911  {csn 4585  {cpr 4587  {ctp 4589

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 3446  df-un 3916  df-ss 3928  df-pr 4588  df-tp 4590

This theorem is referenced by:  fr3nr  7728  rngplusg  17239  srngplusg  17250  lmodplusg  17266  ipsaddg  17277  ipsvsca  17280  phlplusg  17287  topgrpplusg  17302  otpstset  17317  odrngplusg  17344  odrngle  17347  prdsplusg  17397  prdsvsca  17399  prdsle  17401  imasplusg  17456  imasvsca  17459  imasle  17462  fuchom  17906  setchomfval  18021  catchomfval  18044  estrchomfval  18067  xpchomfval  18120  mpocnfldadd  21301  cnfldle  21307  cnfldaddOLD  21316  cnfldleOLD  21320  psrplusg  21878  psrvscafval  21890  trkgdist  28426  rlocaddval  33235  idlsrgplusg  33469  algaddg  43157  clsk1indlem4  44026  rngchomfvalALTV  48248  ringchomfvalALTV  48282  cathomfval  49209  mndtchom  49566