Theorem snsstp2 4778

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 4776	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4179	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3922	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4593	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3962	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

This proof depends on syntax axioms:   ⊆ wss 3900   ∪ cun 4152  {csn 4588  {cpr 4590  {ctp 4592

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-pr 4591  df-tp 4593

This theorem is used by:  fr3nr  7818  rngplusg  17517  srngplusg  17528  lmodplusg  17544  ipsaddg  17555  ipsvsca  17558  phlplusg  17565  topgrpplusg  17580  otpstset  17595  odrngplusg  17622  odrngle  17625  prdsplusg  17679  prdsvsca  17681  prdsle  17683  imasplusg  17739  imasvsca  17742  imasle  17745  fuchom  18189  setchomfval  18304  catchomfval  18327  estrchomfval  18350  xpchomfval  18403  mpocnfldadd  21734  cnfldle  21740  psrplusg  22300  psrvscafval  22311  trkgdist  28965  angmgmlem  29452  rlocaddval  33929  idlsrgplusg  34141  algaddg  44438  clsk1indlem4  45305  rngchomfvalALTV  49637  ringchomfvalALTV  49671  cathomfval  50680  mndtchom  51053