Theorem snsstp2 4785

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 4783	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4131	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3947	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4596	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3987	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

This proof depends on syntax axioms:   ∪ cun 3904   ⊆ wss 3906  {csn 4591  {cpr 4593  {ctp 4595

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-pr 4594  df-tp 4596

This theorem is used by:  fr3nr  7777  rngplusg  17377  srngplusg  17388  lmodplusg  17404  ipsaddg  17415  ipsvsca  17418  phlplusg  17425  topgrpplusg  17440  otpstset  17455  odrngplusg  17482  odrngle  17485  prdsplusg  17535  prdsvsca  17537  prdsle  17539  imasplusg  17595  imasvsca  17598  imasle  17601  fuchom  18045  setchomfval  18160  catchomfval  18183  estrchomfval  18206  xpchomfval  18259  mpocnfldadd  21579  cnfldle  21585  psrplusg  22139  psrvscafval  22150  trkgdist  28768  rlocaddval  33655  idlsrgplusg  33861  algaddg  43962  clsk1indlem4  44830  rngchomfvalALTV  49091  ringchomfvalALTV  49125  cathomfval  50064  mndtchom  50421