MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snsstp2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 snsspr2 4816 . . 3 {𝐵} ⊆ {𝐴, 𝐵}
2 ssun1 4170 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3989 . 2 {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4631 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtrri 4017 1 {𝐵} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator