Theorem snsstp2 4748

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 4746	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4107	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3924	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4560	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3964	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4555  {cpr 4557  {ctp 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-pr 4558  df-tp 4560

This theorem is referenced by:  fr3nr  7715  rngplusg  17254  srngplusg  17265  lmodplusg  17281  ipsaddg  17292  ipsvsca  17295  phlplusg  17302  topgrpplusg  17317  otpstset  17332  odrngplusg  17359  odrngle  17362  prdsplusg  17412  prdsvsca  17414  prdsle  17416  imasplusg  17472  imasvsca  17475  imasle  17478  fuchom  17922  setchomfval  18037  catchomfval  18060  estrchomfval  18083  xpchomfval  18136  mpocnfldadd  21352  cnfldle  21358  psrplusg  21912  psrvscafval  21923  trkgdist  28532  rlocaddval  33349  idlsrgplusg  33588  algaddg  43620  clsk1indlem4  44488  rngchomfvalALTV  48758  ringchomfvalALTV  48792  cathomfval  49717  mndtchom  50074