MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimdv Unicode version

Theorem exlimdv 1724
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 1910. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1747, ax-7 1790. (Revised by Wolf Lammen, 4-Dec-2017.)
Hypothesis
Ref Expression
exlimdv.1
Assertion
Ref Expression
exlimdv
Distinct variable groups:   ,   ,

Proof of Theorem exlimdv
StepHypRef Expression
1 exlimdv.1 . . 3
21eximdv 1710 . 2
3 ax5e 1706 . 2
42, 3syl6 33 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1612
This theorem is referenced by:  exlimdvv  1725  exlimddv  1726  axc9lem1  2001  nfeqf  2045  ax12v2  2083  sbcom2  2189  ax12eq  2271  ax12el  2272  ax12inda  2278  ax12v2-o  2279  tpid3g  4145  sssn  4188  reusv2lem2  4654  ralxfr2d  4668  euotd  4753  wefrc  4878  wereu2  4881  onfr  4922  releldmb  5242  relelrnb  5243  elres  5314  iss  5326  dffv2  5946  dff3  6044  elunirn  6163  isomin  6233  isofrlem  6236  ovmpt4g  6425  soex  6743  f1oweALT  6784  op1steq  6842  fo2ndf  6907  mpt2xopynvov0g  6961  reldmtpos  6982  rntpos  6987  erdisj  7378  map0g  7478  resixpfo  7527  domdifsn  7620  xpdom3  7635  domunsncan  7637  enfixsn  7646  fodomr  7688  mapdom2  7708  mapdom3  7709  phplem4  7719  php3  7723  sucdom2  7734  pssnn  7758  ssfi  7760  domfi  7761  findcard2  7780  ac6sfi  7784  isfinite2  7798  xpfi  7811  domunfican  7813  fiint  7817  fodomfib  7820  mapfien2  7888  marypha1lem  7913  ordiso  7962  hartogslem1  7988  brwdom2  8020  wdomtr  8022  brwdom3  8029  unwdomg  8031  xpwdomg  8032  unxpwdom2  8035  inf3lem2  8067  epfrs  8183  tcmin  8193  cplem1  8328  pm54.43  8402  dfac8alem  8431  dfac8b  8433  dfac8clem  8434  ac10ct  8436  acni2  8448  acndom  8453  numwdom  8461  wdomfil  8463  wdomnumr  8466  iunfictbso  8516  dfac2  8532  dfac9  8537  kmlem13  8563  cdainf  8593  fictb  8646  cfeq0  8657  cff1  8659  cfflb  8660  cofsmo  8670  cfsmolem  8671  coftr  8674  infpssr  8709  fin4en1  8710  fin23lem7  8717  isf34lem4  8778  axcc3  8839  domtriomlem  8843  axdc2lem  8849  axdc3lem2  8852  axdc3lem4  8854  axdc4lem  8856  ac6num  8880  ttukeylem6  8915  ttukeyg  8918  fodomb  8925  iundom2g  8936  alephreg  8978  fpwwe2lem11  9039  fpwwe2lem12  9040  canthp1  9053  pwfseq  9063  gruen  9211  grudomon  9216  gruina  9217  grur1  9219  ltexnq  9374  ltbtwnnq  9377  genpn0  9402  psslinpr  9430  prlem934  9432  ltaddpr  9433  ltexprlem2  9436  ltexprlem6  9440  ltexprlem7  9441  reclem2pr  9447  reclem4pr  9449  suplem1pr  9451  sup2  10524  supmul1  10533  infmrcl  10547  negn0  11197  zsupss  11200  fiinfnf1o  12423  hashfun  12495  hashf1  12506  rlimdm  13374  climcau  13493  caucvgb  13502  summolem2  13538  zsum  13540  sumz  13544  fsumf1o  13545  fsumss  13547  fsumcl2lem  13553  fsumadd  13561  fsummulc2  13599  fsumconst  13605  fsumrelem  13621  ntrivcvg  13706  prodmolem2  13742  zprod  13744  prod1  13751  fprodf1o  13753  fprodss  13755  fprodcl2lem  13757  fprodmul  13765  fproddiv  13766  fprodconst  13782  fprodn0  13783  ruclem13  13975  4sqlem12  14474  vdwapun  14492  vdwlem9  14507  vdwlem10  14508  ramz  14543  ramub1  14546  firest  14830  mremre  15001  isacs2  15050  iscatd2  15078  sscfn1  15186  sscfn2  15187  gsumval2a  15906  symggen  16495  cyggex2  16899  gsumval3OLD  16908  gsumval3  16911  gsumzres  16914  gsumzcl2  16915  gsumzf1o  16917  gsumzresOLD  16918  gsumzclOLD  16919  gsumzf1oOLD  16920  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumconst  16954  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzoppg  16967  gsumzoppgOLD  16968  gsum2d2  17002  pgpfac1lem5  17130  ablfaclem3  17138  lss0cl  17593  lspsnat  17791  cnsubrg  18478  gsumfsum  18484  obslbs  18761  lmiclbs  18872  lmisfree  18877  mdetdiaglem  19100  mdet0  19108  eltg3  19463  tgtop  19475  tgidm  19482  ppttop  19508  toponmre  19594  tgrest  19660  neitr  19681  tgcn  19753  cmpsublem  19899  cmpsub  19900  iunconlem  19928  uncon  19930  1stcfb  19946  2ndcctbss  19956  2ndcdisj  19957  1stcelcls  19962  1stccnp  19963  locfincmp  20027  comppfsc  20033  1stckgen  20055  ptuni2  20077  ptbasfi  20082  ptpjopn  20113  ptclsg  20116  ptcnp  20123  prdstopn  20129  txindis  20135  txtube  20141  txcmplem1  20142  txcmplem2  20143  xkococnlem  20160  txcon  20190  trfbas2  20344  filtop  20356  filcon  20384  filssufilg  20412  fmfnfm  20459  ufldom  20463  hauspwpwf1  20488  alexsubALTlem3  20549  alexsubALT  20551  ptcmplem2  20553  tmdgsum2  20595  tgptsmscld  20653  ustfilxp  20715  xbln0  20917  opnreen  21336  metdsre  21357  cnheibor  21455  phtpc01  21496  cfilfcls  21713  cmetcaulem  21727  iscmet3  21732  ovolctb  21901  ovoliunlem3  21915  ovoliunnul  21918  ovolicc2lem5  21932  ovolicc2  21933  dyadmbl  22009  vitali  22022  itg11  22098  bddmulibl  22245  perfdvf  22307  dvcnp2  22323  dvlip  22394  dvne0  22412  fta1g  22568  fta1  22704  ulmcau  22790  pserulm  22817  wilthlem2  23343  dchrvmasumif  23688  rpvmasum2  23697  dchrisum0re  23698  dchrisum0lem3  23704  dchrisum0  23705  dchrmusum  23709  dchrvmasum  23710  axcontlem10  24276  usgrafisindb1  24409  wlkiswwlk  24698  wlklniswwlkn  24701  clwlkisclwwlklem0  24788  clwlkfoclwwlk  24845  frgra3vlem2  25001  spansncvi  26570  reff  27842  locfinreflem  27843  cmpcref  27853  fmcncfil  27913  volmeas  28203  derangenlem  28615  cvmsss2  28719  cvmopnlem  28723  cvmfolem  28724  cvmliftmolem2  28727  cvmliftlem15  28743  cvmlift2lem10  28757  cvmlift3lem8  28771  rtrclreclem.trans  29069  fundmpss  29196  frmin  29322  wfrlem12  29354  frrlem11  29399  nocvxmin  29451  wl-sbcom2d  30011  supaddc  30041  heicant  30049  itg2addnclem  30066  fnessref  30175  refssfne  30176  neibastop2lem  30178  neibastop2  30179  fnemeet2  30185  fnejoin2  30187  tailfb  30195  sdclem1  30236  fdc  30238  istotbnd3  30267  sstotbnd2  30270  prdsbnd2  30291  heibor1lem  30305  heiborlem1  30307  heiborlem10  30316  heibor  30317  riscer  30391  divrngidl  30425  prtlem17  30617  mapfien2OLD  31042  fsumnncl  31572  stoweidlem43  31825  stoweidlem48  31830  stoweidlem57  31839  stoweidlem60  31842  rlimdmafv  32262  usgo1s0ALT  32437  usgo1s0  32442  mgmpropd  32463  c0snmgmhm  32720  onfrALT  33321  chordthmALT  33733  bnj849  33983  bj-axc15v  34330  osumcllem8N  35687  pexmidlem5N  35698  mapdrvallem2  37372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator