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

Theorem ssdifssd 4122
Description: If 𝐴 is contained in 𝐵, then (𝐴𝐶) is also contained in 𝐵. Deduction form of ssdifss 4115. (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 4115 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3936  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-dif 3942  df-in 3946  df-ss 3955
This theorem is referenced by:  unblem1  8762  fin23lem26  9739  fin23lem29  9755  isf32lem8  9774  fprodfvdvdsd  15675  mrieqvlemd  16892  mrieqv2d  16902  mrissmrid  16904  mreexmrid  16906  mreexexlem2d  16908  mreexexlem4d  16910  acsfiindd  17779  ablfac1eulem  19116  cntzsdrg  19503  lbspss  19776  lspsolv  19837  lsppratlem3  19843  lsppratlem4  19844  lspprat  19847  islbs2  19848  islbs3  19849  lbsextlem2  19853  lbsextlem3  19854  lbsextlem4  19855  lpss3  21670  islp3  21672  neitr  21706  restlp  21709  lpcls  21890  qtoprest  22243  ufinffr  22455  cldsubg  22636  xrge0gsumle  23358  bcthlem5  23848  rrxmval  23925  cmmbl  24052  nulmbl2  24054  shftmbl  24056  iundisj2  24067  uniiccdif  24096  uniiccmbl  24108  itg1val2  24202  itg1cl  24203  itg1ge0  24204  i1fadd  24213  itg1addlem5  24218  i1fmulc  24221  itg1mulc  24222  itg10a  24228  itg1ge0a  24229  itg1climres  24232  mbfi1fseqlem4  24236  itgss3  24332  limcdif  24391  limcnlp  24393  limcmpt2  24399  perfdvf  24418  dvcnp2  24434  dvaddbr  24452  dvmulbr  24453  dvferm1  24499  dvferm2  24501  ftc1lem6  24555  ig1peu  24682  ig1pdvds  24687  taylthlem1  24878  taylthlem2  24879  ulmdvlem3  24907  rlimcnp  25459  wilthlem2  25562  elpwdifcl  30203  iundisj2f  30257  ofpreima2  30328  iundisj2fi  30435  tocyccntz  30702  0nellinds  30851  lindsunlem  30908  lbsdiflsp0  30910  omsmeas  31469  eulerpartlemgs2  31526  ballotlemfrc  31672  hgt750lemd  31807  hgt750leme  31817  cvmscld  32406  unbdqndv1  33733  lindsadd  34754  lindsenlbs  34756  ftc1cnnc  34835  lsatfixedN  36014  dochsnkr  38477  hdmaprnlem4tN  38857  supminfxr2  41612  limcrecl  41777  cnrefiisplem  41977  fperdvper  42070  ismbl3  42139  ovolsplit  42141  ismbl4  42146  stoweidlem57  42210  dirkercncflem3  42258  fourierdlem42  42302  fourierdlem46  42305  fourierdlem62  42321  caragenuncllem  42662  caragendifcl  42664  omelesplit  42668  carageniuncllem2  42672  carageniuncl  42673  caragenel2d  42682  hspmbllem3  42778  hspmbl  42779  ovnsplit  42798  vonvolmbllem  42810  vonvolmbl  42811  c0rnghm  44018  lincdifsn  44313  lindslinindsimp1  44346  lincresunit3lem2  44369
  Copyright terms: Public domain W3C validator