Theorem snsstp2 4787

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

Syntax hints:   ∪ cun 3911   ⊆ wss 3913  {csn 4594  {cpr 4596  {ctp 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-pr 4597  df-tp 4599

This theorem is referenced by:  fr3nr  7771  rngplusg  17353  srngplusg  17364  lmodplusg  17380  ipsaddg  17391  ipsvsca  17394  phlplusg  17401  topgrpplusg  17416  otpstset  17431  odrngplusg  17458  odrngle  17461  prdsplusg  17511  prdsvsca  17513  prdsle  17515  imasplusg  17571  imasvsca  17574  imasle  17577  fuchom  18021  setchomfval  18136  catchomfval  18159  estrchomfval  18182  xpchomfval  18235  mpocnfldadd  21496  cnfldle  21502  psrplusg  22056  psrvscafval  22067  trkgdist  28681  rlocaddval  33530  idlsrgplusg  33740  algaddg  43794  clsk1indlem4  44662  rngchomfvalALTV  48921  ringchomfvalALTV  48955  cathomfval  49890  mndtchom  50247