Theorem snsstp2 4775

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

Syntax hints:   ∪ cun 3902   ⊆ wss 3904  {csn 4582  {cpr 4584  {ctp 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-pr 4585  df-tp 4587

This theorem is referenced by:  fr3nr  7755  rngplusg  17329  srngplusg  17340  lmodplusg  17356  ipsaddg  17367  ipsvsca  17370  phlplusg  17377  topgrpplusg  17392  otpstset  17407  odrngplusg  17434  odrngle  17437  prdsplusg  17487  prdsvsca  17489  prdsle  17491  imasplusg  17547  imasvsca  17550  imasle  17553  fuchom  17997  setchomfval  18112  catchomfval  18135  estrchomfval  18158  xpchomfval  18211  mpocnfldadd  21429  cnfldle  21435  psrplusg  21989  psrvscafval  22000  trkgdist  28615  rlocaddval  33450  idlsrgplusg  33701  algaddg  43752  clsk1indlem4  44620  rngchomfvalALTV  48889  ringchomfvalALTV  48923  cathomfval  49848  mndtchom  50205