Theorem snsstp2 4827

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 4825	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4181	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3999	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4639	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 4027	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3955   ⊆ wss 3957  {csn 4634  {cpr 4636  {ctp 4638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-un 3962  df-ss 3974  df-pr 4637  df-tp 4639

This theorem is referenced by:  fr3nr  7786  rngplusg  17335  srngplusg  17346  lmodplusg  17362  ipsaddg  17373  ipsvsca  17376  phlplusg  17383  topgrpplusg  17398  otpstset  17413  odrngplusg  17440  odrngle  17443  prdsplusg  17494  prdsvsca  17496  prdsle  17498  imasplusg  17553  imasvsca  17556  imasle  17559  fuchom  18006  fuchomOLD  18007  setchomfval  18122  catchomfval  18145  estrchomfval  18170  xpchomfval  18224  mpocnfldadd  21370  cnfldle  21376  cnfldaddOLD  21385  cnfldleOLD  21389  psrplusg  21967  psrvscafval  21979  trkgdist  28396  rlocaddval  33153  idlsrgplusg  33411  algaddg  42901  clsk1indlem4  43772  rngchomfvalALTV  47715  ringchomfvalALTV  47749  mndtchom  48482