Theorem snsstp2 4707

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 4705	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4077	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3901	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4527	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3929	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3856   ⊆ wss 3858  {csn 4522  {cpr 4524  {ctp 4526

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-in 3865  df-ss 3875  df-pr 4525  df-tp 4527

This theorem is referenced by:  fr3nr  7493  rngplusg  16679  srngplusg  16687  lmodplusg  16696  ipsaddg  16703  ipsvsca  16706  phlplusg  16713  topgrpplusg  16721  otpstset  16728  odrngplusg  16739  odrngle  16742  prdsplusg  16789  prdsvsca  16791  prdsle  16793  imasplusg  16848  imasvsca  16851  imasle  16854  fuchom  17290  setchomfval  17405  catchomfval  17424  estrchomfval  17442  xpchomfval  17495  cnfldadd  20171  cnfldle  20175  psrplusg  20709  psrvscafval  20718  trkgdist  26339  idlsrgplusg  31171  algaddg  40496  clsk1indlem4  41120  rngchomfvalALTV  44975  ringchomfvalALTV  45038