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

Theorem ssdifssd 3892
Description: If 𝐴 is contained in 𝐵, then (𝐴𝐶) is also contained in 𝐵. Deduction form of ssdifss 3885. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
ssdifd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
ssdifssd (𝜑 → (𝐴𝐶) ⊆ 𝐵)

Proof of Theorem ssdifssd
StepHypRef Expression
1 ssdifd.1 . 2 (𝜑𝐴𝐵)
2 ssdifss 3885 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3713  wss 3716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-dif 3719  df-in 3723  df-ss 3730
This theorem is referenced by:  unblem1  8380  fin23lem26  9360  fin23lem29  9376  isf32lem8  9395  fprodfvdvdsd  15281  mrieqvlemd  16512  mrieqv2d  16522  mrissmrid  16524  mreexmrid  16526  mreexexlem2d  16528  mreexexlem4d  16530  acsfiindd  17399  ablfac1eulem  18692  lbspss  19305  lspsolv  19366  lsppratlem3  19372  lsppratlem4  19373  lspprat  19376  islbs2  19377  islbs3  19378  lbsextlem2  19382  lbsextlem3  19383  lbsextlem4  19384  lpss3  21171  islp3  21173  neitr  21207  restlp  21210  lpcls  21391  qtoprest  21743  ufinffr  21955  cldsubg  22136  xrge0gsumle  22858  bcthlem5  23346  rrxmval  23409  cmmbl  23523  nulmbl2  23525  shftmbl  23527  iundisj2  23538  uniiccdif  23567  uniiccmbl  23579  itg1val2  23671  itg1cl  23672  itg1ge0  23673  i1fadd  23682  itg1addlem5  23687  i1fmulc  23690  itg1mulc  23691  itg10a  23697  itg1ge0a  23698  itg1climres  23701  mbfi1fseqlem4  23705  itgss3  23801  limcdif  23860  limcnlp  23862  limcmpt2  23868  perfdvf  23887  dvcnp2  23903  dvaddbr  23921  dvmulbr  23922  dvferm1  23968  dvferm2  23970  ftc1lem6  24024  ig1peu  24151  ig1pdvds  24156  taylthlem1  24347  taylthlem2  24348  ulmdvlem3  24376  rlimcnp  24913  wilthlem2  25016  elpwdifcl  29687  iundisj2f  29732  ofpreima2  29797  iundisj2fi  29887  omsmeas  30716  eulerpartlemgs2  30773  ballotlemfrc  30919  hgt750lemd  31057  hgt750leme  31067  cvmscld  31584  unbdqndv1  32827  lindsenlbs  33736  ftc1cnnc  33816  lsatfixedN  34818  dochsnkr  37282  hdmaprnlem4tN  37665  cntzsdrg  38293  supminfxr2  40216  limcrecl  40383  cnrefiisplem  40577  fperdvper  40655  ismbl3  40725  ovolsplit  40727  ismbl4  40732  stoweidlem57  40796  dirkercncflem3  40844  fourierdlem42  40888  fourierdlem46  40891  fourierdlem62  40907  caragenuncllem  41251  caragendifcl  41253  omelesplit  41257  carageniuncllem2  41261  carageniuncl  41262  caragenel2d  41271  hspmbllem3  41367  hspmbl  41368  ovnsplit  41387  vonvolmbllem  41399  vonvolmbl  41400  c0rnghm  42442  lincdifsn  42742  lindslinindsimp1  42775  lincresunit3lem2  42798
  Copyright terms: Public domain W3C validator