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  17902  setchomfval  18017  catchomfval  18040  estrchomfval  18063  xpchomfval  18116  mpocnfldadd  21245  cnfldle  21251  cnfldaddOLD  21260  cnfldleOLD  21264  psrplusg  21821  psrvscafval  21833  trkgdist  28349  rlocaddval  33192  idlsrgplusg  33449  algaddg  43137  clsk1indlem4  44006  rngchomfvalALTV  48228  ringchomfvalALTV  48262  cathomfval  49189  mndtchom  49546