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

Theorem ssdifssd 4107
Description: If 𝐴 is contained in 𝐵, then (𝐴𝐶) is also contained in 𝐵. Deduction form of ssdifss 4100. (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 4100 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3912  wss 3915
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918  df-in 3922  df-ss 3932
This theorem is referenced by:  xpord3pred  8089  unblem1  9246  fin23lem26  10268  fin23lem29  10284  isf32lem8  10303  fprodfvdvdsd  16223  mrieqvlemd  17516  mrieqv2d  17526  mrissmrid  17528  mreexmrid  17530  mreexexlem2d  17532  mreexexlem4d  17534  acsfiindd  18449  ablfac1eulem  19858  cntzsdrg  20285  lbspss  20559  lspsolv  20620  lsppratlem3  20626  lsppratlem4  20627  lspprat  20630  islbs2  20631  islbs3  20632  lbsextlem2  20636  lbsextlem3  20637  lbsextlem4  20638  lpss3  22511  islp3  22513  neitr  22547  restlp  22550  lpcls  22731  qtoprest  23084  ufinffr  23296  cldsubg  23478  xrge0gsumle  24212  bcthlem5  24708  rrxmval  24785  cmmbl  24914  nulmbl2  24916  shftmbl  24918  iundisj2  24929  uniiccdif  24958  uniiccmbl  24970  itg1val2  25064  itg1cl  25065  itg1ge0  25066  i1fadd  25075  itg1addlem5  25081  i1fmulc  25084  itg1mulc  25085  itg10a  25091  itg1ge0a  25092  itg1climres  25095  mbfi1fseqlem4  25099  itgss3  25195  limcdif  25256  limcnlp  25258  limcmpt2  25264  perfdvf  25283  dvcnp2  25300  dvaddbr  25318  dvmulbr  25319  dvferm1  25365  dvferm2  25367  ftc1lem6  25421  ig1peu  25552  ig1pdvds  25557  taylthlem1  25748  taylthlem2  25749  ulmdvlem3  25777  rlimcnp  26331  wilthlem2  26434  newf  27210  elpwdifcl  31496  iundisj2f  31550  ofpreima2  31624  iundisj2fi  31742  tocyccntz  32035  0nellinds  32199  elrspunidl  32243  lindsunlem  32359  lbsdiflsp0  32361  omsmeas  32963  eulerpartlemgs2  33020  ballotlemfrc  33166  hgt750lemd  33301  hgt750leme  33311  cvmscld  33907  unbdqndv1  35000  lindsadd  36100  lindsenlbs  36102  ftc1cnnc  36179  lsatfixedN  37500  dochsnkr  39964  hdmaprnlem4tN  40344  prjcrv0  41000  supminfxr2  43778  limcrecl  43944  cnrefiisplem  44144  fperdvper  44234  ismbl3  44301  ovolsplit  44303  ismbl4  44308  stoweidlem57  44372  dirkercncflem3  44420  fourierdlem42  44464  fourierdlem46  44467  fourierdlem62  44483  caragenuncllem  44827  caragendifcl  44829  omelesplit  44833  carageniuncllem2  44837  carageniuncl  44838  caragenel2d  44847  hspmbllem3  44943  hspmbl  44944  ovnsplit  44963  vonvolmbllem  44975  vonvolmbl  44976  c0rnghm  46285  lincdifsn  46579  lindslinindsimp1  46612  lincresunit3lem2  46635
  Copyright terms: Public domain W3C validator