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

Theorem exlimdv 1643
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. Revised to remove dependency on ax-9 1662 and ax-8 1683. (Contributed by NM, 27-Apr-1994.) (Revised by Wolf Lammen, 4-Dec-2017.)
Hypothesis
Ref Expression
exlimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
exlimdv  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Distinct variable groups:    ch, x    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem exlimdv
StepHypRef Expression
1 exlimdv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21eximdv 1629 . 2  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
3 ax17e 1625 . 2  |-  ( E. x ch  ->  ch )
42, 3syl6 31 1  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1547
This theorem is referenced by:  exlimdvv  1644  exlimddv  1645  ax10OLD  1998  ax11v2  2025  ax11v2OLD  2026  ax11eq  2251  ax11el  2252  ax11inda  2258  ax11v2-o  2259  tpid3g  3887  sssn  3925  euotd  4425  wefrc  4544  wereu2  4547  onfr  4588  reusv2lem2  4692  ralxfr2d  4706  releldmb  5071  relelrnb  5072  elres  5148  iss  5156  soex  5286  dffv2  5763  dff3  5849  elunirnALT  5967  isomin  6024  isofrlem  6027  f1oweALT  6041  ovmpt4g  6163  op1steq  6358  fo2ndf  6420  mpt2xopynvov0g  6432  reldmtpos  6454  rntpos  6459  erdisj  6919  map0g  7020  resixpfo  7067  domdifsn  7158  xpdom3  7173  domunsncan  7175  fodomr  7225  mapdom2  7245  mapdom3  7246  phplem4  7256  php3  7260  sucdom2  7270  pssnn  7294  ssfi  7296  domfi  7297  findcard2  7315  ac6sfi  7318  isfinite2  7332  xpfi  7345  domunfican  7346  fiint  7350  fodomfib  7353  marypha1lem  7404  ordiso  7449  hartogslem1  7475  brwdom2  7505  wdomtr  7507  brwdom3  7514  unwdomg  7516  xpwdomg  7517  unxpwdom2  7520  inf3lem2  7548  epfrs  7631  tcmin  7644  cplem1  7777  pm54.43  7851  dfac8alem  7874  dfac8b  7876  dfac8clem  7877  ac10ct  7879  acni2  7891  acndom  7896  numwdom  7904  wdomfil  7906  wdomnumr  7909  iunfictbso  7959  dfac2  7975  dfac9  7980  kmlem13  8006  cdainf  8036  fictb  8089  cfeq0  8100  cff1  8102  cfflb  8103  cofsmo  8113  cfsmolem  8114  coftr  8117  infpssr  8152  fin4en1  8153  fin23lem7  8160  isf34lem4  8221  axcc3  8282  domtriomlem  8286  axdc2lem  8292  axdc3lem2  8295  axdc3lem4  8297  axdc4lem  8299  ac6num  8323  ttukeylem6  8358  ttukeyg  8361  fodomb  8368  iundom2g  8379  alephreg  8421  fpwwe2lem11  8479  fpwwe2lem12  8480  canthp1  8493  pwfseq  8503  gruen  8651  grudomon  8656  gruina  8657  grur1  8659  ltexnq  8816  ltbtwnnq  8819  genpn0  8844  psslinpr  8872  prlem934  8874  ltaddpr  8875  ltexprlem2  8878  ltexprlem6  8882  ltexprlem7  8883  reclem2pr  8889  reclem4pr  8891  suplem1pr  8893  sup2  9928  supmul1  9937  infmrcl  9951  negn0  10526  zsupss  10529  fiinfnf1o  11597  hashfun  11663  hashf1  11669  rlimdm  12308  climcau  12427  caucvgb  12436  summolem2  12473  zsum  12475  sumz  12479  fsumf1o  12480  fsumss  12482  fsumcl2lem  12488  fsumadd  12495  fsummulc2  12530  fsumconst  12536  fsumrelem  12549  ruclem13  12804  4sqlem12  13287  vdwapun  13305  vdwlem9  13320  vdwlem10  13321  ramz  13356  ramub1  13359  firest  13623  mremre  13792  isacs2  13841  iscatd2  13869  sscfn1  13980  sscfn2  13981  gsumval2a  14745  cyggex2  15469  gsumval3  15477  gsumzres  15480  gsumzcl  15481  gsumzf1o  15482  gsumzaddlem  15489  gsumconst  15495  gsumzmhm  15496  gsumzoppg  15502  gsum2d2  15511  pgpfac1lem5  15600  ablfaclem3  15608  lss0cl  15986  lspsnat  16180  cnsubrg  16722  gsumfsum  16729  obslbs  16920  eltg3  16990  tgtop  17001  tgidm  17008  ppttop  17034  toponmre  17120  tgrest  17185  neitr  17206  tgcn  17278  cmpsublem  17424  cmpsub  17425  iunconlem  17451  uncon  17453  1stcfb  17469  2ndcctbss  17479  2ndcdisj  17480  1stcelcls  17485  1stccnp  17486  1stckgen  17547  ptuni2  17569  ptbasfi  17574  ptpjopn  17605  ptclsg  17608  ptcnp  17615  prdstopn  17621  txindis  17627  txtube  17633  txcmplem1  17634  txcmplem2  17635  xkococnlem  17652  txcon  17682  trfbas2  17836  filtop  17848  filcon  17876  filssufilg  17904  fmfnfm  17951  ufldom  17955  hauspwpwf1  17980  alexsubALTlem3  18041  alexsubALT  18043  ptcmplem2  18045  tmdgsum2  18087  tgptsmscld  18141  ustfilxp  18203  xbln0  18405  opnreen  18823  metdsre  18844  cnheibor  18941  phtpc01  18982  cfilfcls  19188  cmetcaulem  19202  iscmet3  19207  ovolctb  19347  ovoliunlem3  19361  ovoliunnul  19364  ovolicc2lem5  19378  ovolicc2  19379  dyadmbl  19453  vitali  19466  itg11  19544  bddmulibl  19691  perfdvf  19751  dvcnp2  19767  dvlip  19838  dvne0  19856  fta1g  20051  fta1  20186  ulmcau  20272  pserulm  20299  wilthlem2  20813  dchrvmasumif  21158  rpvmasum2  21167  dchrisum0re  21168  dchrisum0lem3  21174  dchrisum0  21175  dchrmusum  21179  dchrvmasum  21180  usgrafisindb1  21384  spansncvi  23115  fmcncfil  24278  volmeas  24548  derangenlem  24818  cvmsss2  24922  cvmopnlem  24926  cvmfolem  24927  cvmliftmolem2  24930  cvmliftlem15  24946  cvmlift2lem10  24960  cvmlift3lem8  24974  rtrclreclem.trans  25107  ntrivcvg  25186  prodmolem2  25222  zprod  25224  prod1  25231  fprodf1o  25233  fprodss  25235  fprodcl2lem  25237  fprodmul  25245  fproddiv  25246  fprodconst  25263  fprodn0  25264  fundmpss  25344  frmin  25464  wfrlem12  25489  frrlem11  25515  nocvxmin  25567  axcontlem10  25824  supaddc  26145  itg2addnclem  26163  fnessref  26271  refssfne  26272  locfincmp  26282  comppfsc  26285  neibastop2lem  26287  neibastop2  26288  fnemeet2  26294  fnejoin2  26296  tailfb  26304  sdclem1  26345  fdc  26347  istotbnd3  26378  sstotbnd2  26381  prdsbnd2  26402  heibor1lem  26416  heiborlem1  26418  heiborlem10  26427  heibor  26428  riscer  26502  divrngidl  26536  prtlem17  26623  enfixsn  27133  mapfien2  27134  lmiclbs  27183  lmisfree  27188  symggen  27287  stoweidlem43  27667  stoweidlem48  27672  stoweidlem57  27681  stoweidlem60  27684  rlimdmafv  27916  frgra3vlem2  28113  onfrALT  28354  chordthmALT  28764  bnj849  29014  ax10NEW7  29191  ax11v2NEW7  29246  osumcllem8N  30457  pexmidlem5N  30468  mapdrvallem2  32140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator