Theorem snsstp2 4768

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 4766	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4129	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3945	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4582	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3985	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {csn 4577  {cpr 4579  {ctp 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920  df-pr 4580  df-tp 4582

This theorem is referenced by:  fr3nr  7708  rngplusg  17204  srngplusg  17215  lmodplusg  17231  ipsaddg  17242  ipsvsca  17245  phlplusg  17252  topgrpplusg  17267  otpstset  17282  odrngplusg  17309  odrngle  17312  prdsplusg  17362  prdsvsca  17364  prdsle  17366  imasplusg  17421  imasvsca  17424  imasle  17427  fuchom  17871  setchomfval  17986  catchomfval  18009  estrchomfval  18032  xpchomfval  18085  mpocnfldadd  21266  cnfldle  21272  cnfldaddOLD  21281  cnfldleOLD  21285  psrplusg  21843  psrvscafval  21855  trkgdist  28391  rlocaddval  33208  idlsrgplusg  33442  algaddg  43152  clsk1indlem4  44021  rngchomfvalALTV  48255  ringchomfvalALTV  48289  cathomfval  49216  mndtchom  49573