Theorem snsstp2 4821

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 4819	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4173	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3992	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4634	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 4020	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3947   ⊆ wss 3949  {csn 4629  {cpr 4631  {ctp 4633

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-pr 4632  df-tp 4634

This theorem is referenced by:  fr3nr  7759  rngplusg  17245  srngplusg  17256  lmodplusg  17272  ipsaddg  17283  ipsvsca  17286  phlplusg  17293  topgrpplusg  17308  otpstset  17323  odrngplusg  17350  odrngle  17353  prdsplusg  17404  prdsvsca  17406  prdsle  17408  imasplusg  17463  imasvsca  17466  imasle  17469  fuchom  17913  fuchomOLD  17914  setchomfval  18029  catchomfval  18052  estrchomfval  18077  xpchomfval  18131  cnfldadd  20949  cnfldle  20953  psrplusg  21500  psrvscafval  21509  trkgdist  27697  idlsrgplusg  32619  algaddg  41921  clsk1indlem4  42795  rngchomfvalALTV  46882  ringchomfvalALTV  46945  mndtchom  47710