Theorem snsstp2 4772

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

This proof depends on syntax axioms:   ⊆ wss 3896   ∪ cun 4148  {csn 4584  {cpr 4586  {ctp 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150  df-pr 4587  df-tp 4589

This theorem is used by:  fr3nr  7790  rngplusg  17480  srngplusg  17491  lmodplusg  17507  ipsaddg  17518  ipsvsca  17521  phlplusg  17528  topgrpplusg  17543  otpstset  17558  odrngplusg  17585  odrngle  17588  prdsplusg  17638  prdsvsca  17640  prdsle  17642  imasplusg  17698  imasvsca  17701  imasle  17704  fuchom  18148  setchomfval  18263  catchomfval  18286  estrchomfval  18309  xpchomfval  18362  mpocnfldadd  21692  cnfldle  21698  psrplusg  22254  psrvscafval  22265  trkgdist  28917  angmgmlem  29404  rlocaddval  33880  idlsrgplusg  34087  algaddg  44314  clsk1indlem4  45181  rngchomfvalALTV  49500  ringchomfvalALTV  49534  cathomfval  50485  mndtchom  50858