Theorem snsstp2 4348

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 4346	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 3776	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3612	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4182	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtr4i 3638	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3572   ⊆ wss 3574  {csn 4177  {cpr 4179  {ctp 4181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-pr 4180  df-tp 4182

This theorem is referenced by:  fr3nr  6979  rngplusg  16002  srngplusg  16010  lmodplusg  16019  ipsaddg  16026  ipsvsca  16029  phlplusg  16036  topgrpplusg  16044  otpstset  16053  otpstsetOLD  16057  odrngplusg  16068  odrngle  16071  prdsplusg  16118  prdsvsca  16120  prdsle  16122  imasplusg  16177  imasvsca  16180  imasle  16183  fuchom  16621  setchomfval  16729  catchomfval  16748  estrchomfval  16766  xpchomfval  16819  psrplusg  19381  psrvscafval  19390  cnfldadd  19751  cnfldle  19755  trkgdist  25345  algaddg  37749  clsk1indlem4  38342  rngchomfvalALTV  41984  ringchomfvalALTV  42047