Theorem snsstp2 4747

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 4745	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4102	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3926	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4563	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3954	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4558  {cpr 4560  {ctp 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-pr 4561  df-tp 4563

This theorem is referenced by:  fr3nr  7600  rngplusg  16936  srngplusg  16947  lmodplusg  16963  ipsaddg  16973  ipsvsca  16976  phlplusg  16983  topgrpplusg  16997  otpstset  17011  odrngplusg  17034  odrngle  17037  prdsplusg  17086  prdsvsca  17088  prdsle  17090  imasplusg  17145  imasvsca  17148  imasle  17151  fuchom  17594  fuchomOLD  17595  setchomfval  17710  catchomfval  17733  estrchomfval  17758  xpchomfval  17812  cnfldadd  20515  cnfldle  20519  psrplusg  21060  psrvscafval  21069  trkgdist  26711  idlsrgplusg  31552  algaddg  40920  clsk1indlem4  41543  rngchomfvalALTV  45430  ringchomfvalALTV  45493  mndtchom  46257