Theorem snsstp2 4818

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 4816	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4170	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3989	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4631	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 4017	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3944   ⊆ wss 3946  {csn 4626  {cpr 4628  {ctp 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3951  df-in 3953  df-ss 3963  df-pr 4629  df-tp 4631

This theorem is referenced by:  fr3nr  7753  rngplusg  17240  srngplusg  17251  lmodplusg  17267  ipsaddg  17278  ipsvsca  17281  phlplusg  17288  topgrpplusg  17303  otpstset  17318  odrngplusg  17345  odrngle  17348  prdsplusg  17399  prdsvsca  17401  prdsle  17403  imasplusg  17458  imasvsca  17461  imasle  17464  fuchom  17908  fuchomOLD  17909  setchomfval  18024  catchomfval  18047  estrchomfval  18072  xpchomfval  18126  cnfldadd  20933  cnfldle  20937  psrplusg  21481  psrvscafval  21490  trkgdist  27676  idlsrgplusg  32570  algaddg  41853  clsk1indlem4  42727  rngchomfvalALTV  46783  ringchomfvalALTV  46846  mndtchom  47611