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

Theorem ssdifssd 3976
Description: If 𝐴 is contained in 𝐵, then (𝐴𝐶) is also contained in 𝐵. Deduction form of ssdifss 3969. (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 3969 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3796  wss 3799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2804
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-v 3417  df-dif 3802  df-in 3806  df-ss 3813
This theorem is referenced by:  unblem1  8482  fin23lem26  9463  fin23lem29  9479  isf32lem8  9498  fprodfvdvdsd  15433  mrieqvlemd  16643  mrieqv2d  16653  mrissmrid  16655  mreexmrid  16657  mreexexlem2d  16659  mreexexlem4d  16661  acsfiindd  17531  ablfac1eulem  18826  lbspss  19442  lspsolv  19504  lsppratlem3  19511  lsppratlem4  19512  lspprat  19515  islbs2  19516  islbs3  19517  lbsextlem2  19521  lbsextlem3  19522  lbsextlem4  19523  lpss3  21320  islp3  21322  neitr  21356  restlp  21359  lpcls  21540  qtoprest  21892  ufinffr  22104  cldsubg  22285  xrge0gsumle  23007  bcthlem5  23497  rrxmval  23574  cmmbl  23701  nulmbl2  23703  shftmbl  23705  iundisj2  23716  uniiccdif  23745  uniiccmbl  23757  itg1val2  23851  itg1cl  23852  itg1ge0  23853  i1fadd  23862  itg1addlem5  23867  i1fmulc  23870  itg1mulc  23871  itg10a  23877  itg1ge0a  23878  itg1climres  23881  mbfi1fseqlem4  23885  itgss3  23981  limcdif  24040  limcnlp  24042  limcmpt2  24048  perfdvf  24067  dvcnp2  24083  dvaddbr  24101  dvmulbr  24102  dvferm1  24148  dvferm2  24150  ftc1lem6  24204  ig1peu  24331  ig1pdvds  24336  taylthlem1  24527  taylthlem2  24528  ulmdvlem3  24556  rlimcnp  25106  wilthlem2  25209  elpwdifcl  29907  iundisj2f  29951  ofpreima2  30016  iundisj2fi  30104  omsmeas  30931  eulerpartlemgs2  30988  ballotlemfrc  31135  hgt750lemd  31276  hgt750leme  31286  cvmscld  31802  unbdqndv1  33032  lindsadd  33947  lindsenlbs  33949  ftc1cnnc  34028  lsatfixedN  35085  dochsnkr  37548  hdmaprnlem4tN  37928  cntzsdrg  38616  supminfxr2  40494  limcrecl  40657  cnrefiisplem  40851  fperdvper  40929  ismbl3  40998  ovolsplit  41000  ismbl4  41005  stoweidlem57  41069  dirkercncflem3  41117  fourierdlem42  41161  fourierdlem46  41164  fourierdlem62  41180  caragenuncllem  41521  caragendifcl  41523  omelesplit  41527  carageniuncllem2  41531  carageniuncl  41532  caragenel2d  41541  hspmbllem3  41637  hspmbl  41638  ovnsplit  41657  vonvolmbllem  41669  vonvolmbl  41670  c0rnghm  42761  lincdifsn  43061  lindslinindsimp1  43094  lincresunit3lem2  43117
  Copyright terms: Public domain W3C validator