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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-pr 4587  df-tp 4589

This theorem is used by:  fr3nr  7772  rngplusg  17386  srngplusg  17397  lmodplusg  17413  ipsaddg  17424  ipsvsca  17427  phlplusg  17434  topgrpplusg  17449  otpstset  17464  odrngplusg  17491  odrngle  17494  prdsplusg  17544  prdsvsca  17546  prdsle  17548  imasplusg  17604  imasvsca  17607  imasle  17610  fuchom  18054  setchomfval  18169  catchomfval  18192  estrchomfval  18215  xpchomfval  18268  mpocnfldadd  21591  cnfldle  21597  psrplusg  22153  psrvscafval  22164  trkgdist  28788  angmgmlem  29275  rlocaddval  33710  idlsrgplusg  33916  algaddg  44017  clsk1indlem4  44885  rngchomfvalALTV  49183  ringchomfvalALTV  49217  cathomfval  50154  mndtchom  50511