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

Theorem exlimdv 1646
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. Revised to remove dependency on ax-9 1666 and ax-8 1687. (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 1632 . 2  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
3 ax17e 1628 . 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 1550
This theorem is referenced by:  exlimdvv  1647  exlimddv  1648  ax10OLD  2032  ax11v2  2078  ax11v2OLD  2079  ax11eq  2270  ax11el  2271  ax11inda  2277  ax11v2-o  2278  tpid3g  3919  sssn  3957  euotd  4457  wefrc  4576  wereu2  4579  onfr  4620  reusv2lem2  4725  ralxfr2d  4739  releldmb  5104  relelrnb  5105  elres  5181  iss  5189  soex  5319  dffv2  5796  dff3  5882  elunirnALT  6000  isomin  6057  isofrlem  6060  f1oweALT  6074  ovmpt4g  6196  op1steq  6391  fo2ndf  6453  mpt2xopynvov0g  6465  reldmtpos  6487  rntpos  6492  erdisj  6952  map0g  7053  resixpfo  7100  domdifsn  7191  xpdom3  7206  domunsncan  7208  fodomr  7258  mapdom2  7278  mapdom3  7279  phplem4  7289  php3  7293  sucdom2  7303  pssnn  7327  ssfi  7329  domfi  7330  findcard2  7348  ac6sfi  7351  isfinite2  7365  xpfi  7378  domunfican  7379  fiint  7383  fodomfib  7386  marypha1lem  7438  ordiso  7485  hartogslem1  7511  brwdom2  7541  wdomtr  7543  brwdom3  7550  unwdomg  7552  xpwdomg  7553  unxpwdom2  7556  inf3lem2  7584  epfrs  7667  tcmin  7680  cplem1  7813  pm54.43  7887  dfac8alem  7910  dfac8b  7912  dfac8clem  7913  ac10ct  7915  acni2  7927  acndom  7932  numwdom  7940  wdomfil  7942  wdomnumr  7945  iunfictbso  7995  dfac2  8011  dfac9  8016  kmlem13  8042  cdainf  8072  fictb  8125  cfeq0  8136  cff1  8138  cfflb  8139  cofsmo  8149  cfsmolem  8150  coftr  8153  infpssr  8188  fin4en1  8189  fin23lem7  8196  isf34lem4  8257  axcc3  8318  domtriomlem  8322  axdc2lem  8328  axdc3lem2  8331  axdc3lem4  8333  axdc4lem  8335  ac6num  8359  ttukeylem6  8394  ttukeyg  8397  fodomb  8404  iundom2g  8415  alephreg  8457  fpwwe2lem11  8515  fpwwe2lem12  8516  canthp1  8529  pwfseq  8539  gruen  8687  grudomon  8692  gruina  8693  grur1  8695  ltexnq  8852  ltbtwnnq  8855  genpn0  8880  psslinpr  8908  prlem934  8910  ltaddpr  8911  ltexprlem2  8914  ltexprlem6  8918  ltexprlem7  8919  reclem2pr  8925  reclem4pr  8927  suplem1pr  8929  sup2  9964  supmul1  9973  infmrcl  9987  negn0  10562  zsupss  10565  fiinfnf1o  11634  hashfun  11700  hashf1  11706  rlimdm  12345  climcau  12464  caucvgb  12473  summolem2  12510  zsum  12512  sumz  12516  fsumf1o  12517  fsumss  12519  fsumcl2lem  12525  fsumadd  12532  fsummulc2  12567  fsumconst  12573  fsumrelem  12586  ruclem13  12841  4sqlem12  13324  vdwapun  13342  vdwlem9  13357  vdwlem10  13358  ramz  13393  ramub1  13396  firest  13660  mremre  13829  isacs2  13878  iscatd2  13906  sscfn1  14017  sscfn2  14018  gsumval2a  14782  cyggex2  15506  gsumval3  15514  gsumzres  15517  gsumzcl  15518  gsumzf1o  15519  gsumzaddlem  15526  gsumconst  15532  gsumzmhm  15533  gsumzoppg  15539  gsum2d2  15548  pgpfac1lem5  15637  ablfaclem3  15645  lss0cl  16023  lspsnat  16217  cnsubrg  16759  gsumfsum  16766  obslbs  16957  eltg3  17027  tgtop  17038  tgidm  17045  ppttop  17071  toponmre  17157  tgrest  17223  neitr  17244  tgcn  17316  cmpsublem  17462  cmpsub  17463  iunconlem  17490  uncon  17492  1stcfb  17508  2ndcctbss  17518  2ndcdisj  17519  1stcelcls  17524  1stccnp  17525  1stckgen  17586  ptuni2  17608  ptbasfi  17613  ptpjopn  17644  ptclsg  17647  ptcnp  17654  prdstopn  17660  txindis  17666  txtube  17672  txcmplem1  17673  txcmplem2  17674  xkococnlem  17691  txcon  17721  trfbas2  17875  filtop  17887  filcon  17915  filssufilg  17943  fmfnfm  17990  ufldom  17994  hauspwpwf1  18019  alexsubALTlem3  18080  alexsubALT  18082  ptcmplem2  18084  tmdgsum2  18126  tgptsmscld  18180  ustfilxp  18242  xbln0  18444  opnreen  18862  metdsre  18883  cnheibor  18980  phtpc01  19021  cfilfcls  19227  cmetcaulem  19241  iscmet3  19246  ovolctb  19386  ovoliunlem3  19400  ovoliunnul  19403  ovolicc2lem5  19417  ovolicc2  19418  dyadmbl  19492  vitali  19505  itg11  19583  bddmulibl  19730  perfdvf  19790  dvcnp2  19806  dvlip  19877  dvne0  19895  fta1g  20090  fta1  20225  ulmcau  20311  pserulm  20338  wilthlem2  20852  dchrvmasumif  21197  rpvmasum2  21206  dchrisum0re  21207  dchrisum0lem3  21213  dchrisum0  21214  dchrmusum  21218  dchrvmasum  21219  usgrafisindb1  21423  spansncvi  23154  fmcncfil  24317  volmeas  24587  derangenlem  24857  cvmsss2  24961  cvmopnlem  24965  cvmfolem  24966  cvmliftmolem2  24969  cvmliftlem15  24985  cvmlift2lem10  24999  cvmlift3lem8  25013  rtrclreclem.trans  25146  ntrivcvg  25225  prodmolem2  25261  zprod  25263  prod1  25270  fprodf1o  25272  fprodss  25274  fprodcl2lem  25276  fprodmul  25284  fproddiv  25285  fprodconst  25302  fprodn0  25303  fundmpss  25390  frmin  25517  wfrlem12  25549  frrlem11  25594  nocvxmin  25646  axcontlem10  25912  supaddc  26237  itg2addnclem  26256  fnessref  26373  refssfne  26374  locfincmp  26384  comppfsc  26387  neibastop2lem  26389  neibastop2  26390  fnemeet2  26396  fnejoin2  26398  tailfb  26406  sdclem1  26447  fdc  26449  istotbnd3  26480  sstotbnd2  26483  prdsbnd2  26504  heibor1lem  26518  heiborlem1  26520  heiborlem10  26529  heibor  26530  riscer  26604  divrngidl  26638  prtlem17  26725  enfixsn  27234  mapfien2  27235  lmiclbs  27284  lmisfree  27289  symggen  27388  stoweidlem43  27768  stoweidlem48  27773  stoweidlem57  27782  stoweidlem60  27785  rlimdmafv  28017  frgra3vlem2  28391  onfrALT  28635  chordthmALT  29045  bnj849  29296  ax10NEW7  29473  ax11v2NEW7  29530  osumcllem8N  30760  pexmidlem5N  30771  mapdrvallem2  32443
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator