Theorem snsstp2 4784

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 4782	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4144	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3959	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4597	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3999	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3915   ⊆ wss 3917  {csn 4592  {cpr 4594  {ctp 4596

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-pr 4595  df-tp 4597

This theorem is referenced by:  fr3nr  7751  rngplusg  17270  srngplusg  17281  lmodplusg  17297  ipsaddg  17308  ipsvsca  17311  phlplusg  17318  topgrpplusg  17333  otpstset  17348  odrngplusg  17375  odrngle  17378  prdsplusg  17428  prdsvsca  17430  prdsle  17432  imasplusg  17487  imasvsca  17490  imasle  17493  fuchom  17933  setchomfval  18048  catchomfval  18071  estrchomfval  18094  xpchomfval  18147  mpocnfldadd  21276  cnfldle  21282  cnfldaddOLD  21291  cnfldleOLD  21295  psrplusg  21852  psrvscafval  21864  trkgdist  28380  rlocaddval  33226  idlsrgplusg  33483  algaddg  43171  clsk1indlem4  44040  rngchomfvalALTV  48259  ringchomfvalALTV  48293  cathomfval  49220  mndtchom  49577