Theorem snsstp2 4750

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 4748	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4106	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3930	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4566	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3958	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3885   ⊆ wss 3887  {csn 4561  {cpr 4563  {ctp 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-pr 4564  df-tp 4566

This theorem is referenced by:  fr3nr  7622  rngplusg  17010  srngplusg  17021  lmodplusg  17037  ipsaddg  17048  ipsvsca  17051  phlplusg  17058  topgrpplusg  17073  otpstset  17088  odrngplusg  17115  odrngle  17118  prdsplusg  17169  prdsvsca  17171  prdsle  17173  imasplusg  17228  imasvsca  17231  imasle  17234  fuchom  17678  fuchomOLD  17679  setchomfval  17794  catchomfval  17817  estrchomfval  17842  xpchomfval  17896  cnfldadd  20602  cnfldle  20606  psrplusg  21150  psrvscafval  21159  trkgdist  26807  idlsrgplusg  31650  algaddg  41004  clsk1indlem4  41654  rngchomfvalALTV  45542  ringchomfvalALTV  45605  mndtchom  46371