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 4124	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3940	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4589	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3980	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

This proof depends on syntax axioms:   ∪ cun 3897   ⊆ wss 3899  {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 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-pr 4587  df-tp 4589

This theorem is used by:  fr3nr  7786  rngplusg  17471  srngplusg  17482  lmodplusg  17498  ipsaddg  17509  ipsvsca  17512  phlplusg  17519  topgrpplusg  17534  otpstset  17549  odrngplusg  17576  odrngle  17579  prdsplusg  17629  prdsvsca  17631  prdsle  17633  imasplusg  17689  imasvsca  17692  imasle  17695  fuchom  18139  setchomfval  18254  catchomfval  18277  estrchomfval  18300  xpchomfval  18353  mpocnfldadd  21683  cnfldle  21689  psrplusg  22245  psrvscafval  22256  trkgdist  28908  angmgmlem  29395  rlocaddval  33830  idlsrgplusg  34037  algaddg  44176  clsk1indlem4  45043  rngchomfvalALTV  49363  ringchomfvalALTV  49397  cathomfval  50334  mndtchom  50691