Theorem snsstp2 4775

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 4773	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4132	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3945	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4587	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3985	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {csn 4582  {cpr 4584  {ctp 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-pr 4585  df-tp 4587

This theorem is referenced by:  fr3nr  7727  rngplusg  17232  srngplusg  17243  lmodplusg  17259  ipsaddg  17270  ipsvsca  17273  phlplusg  17280  topgrpplusg  17295  otpstset  17310  odrngplusg  17337  odrngle  17340  prdsplusg  17390  prdsvsca  17392  prdsle  17394  imasplusg  17450  imasvsca  17453  imasle  17456  fuchom  17900  setchomfval  18015  catchomfval  18038  estrchomfval  18061  xpchomfval  18114  mpocnfldadd  21326  cnfldle  21332  cnfldaddOLD  21341  cnfldleOLD  21345  psrplusg  21904  psrvscafval  21916  trkgdist  28530  rlocaddval  33362  idlsrgplusg  33598  algaddg  43532  clsk1indlem4  44400  rngchomfvalALTV  48627  ringchomfvalALTV  48661  cathomfval  49586  mndtchom  49943