Theorem snsstp2 4821

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 4819	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4187	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 4004	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4635	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 4032	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3960   ⊆ wss 3962  {csn 4630  {cpr 4632  {ctp 4634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-pr 4633  df-tp 4635

This theorem is referenced by:  fr3nr  7790  rngplusg  17345  srngplusg  17356  lmodplusg  17372  ipsaddg  17383  ipsvsca  17386  phlplusg  17393  topgrpplusg  17408  otpstset  17423  odrngplusg  17450  odrngle  17453  prdsplusg  17504  prdsvsca  17506  prdsle  17508  imasplusg  17563  imasvsca  17566  imasle  17569  fuchom  18016  fuchomOLD  18017  setchomfval  18132  catchomfval  18155  estrchomfval  18180  xpchomfval  18234  mpocnfldadd  21386  cnfldle  21392  cnfldaddOLD  21401  cnfldleOLD  21405  psrplusg  21973  psrvscafval  21985  trkgdist  28468  rlocaddval  33254  idlsrgplusg  33512  algaddg  43163  clsk1indlem4  44033  rngchomfvalALTV  48110  ringchomfvalALTV  48144  mndtchom  48892