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

Theorem exlimdv 1626
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 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 1612 . 2  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
3 ax17e 1608 . 2  |-  ( E. x ch  ->  ch )
42, 3syl6 29 1  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531
This theorem is referenced by:  exlimdvv  1627  exlimddv  1628  ax10  1897  ax11v2  1945  ax11eq  2145  ax11el  2146  ax11inda  2152  ax11v2-o  2153  tpid3g  3754  sssn  3788  euotd  4283  wefrc  4403  wereu2  4406  onfr  4447  reusv2lem2  4552  ralxfr2d  4566  releldmb  4929  relelrnb  4930  elres  5006  iss  5014  soex  5138  dffv2  5608  fvmptdv2  5629  dff3  5689  elunirnALT  5795  isomin  5850  isofrlem  5853  f1oweALT  5867  ovmpt4g  5986  op1steq  6180  reldmtpos  6258  rntpos  6263  tfrlem9a  6418  erref  6696  erdisj  6723  map0g  6823  resixpfo  6870  domdifsn  6961  xpdom2  6973  xpdom3  6976  domunsncan  6978  domunsn  7027  fodomr  7028  mapdom1  7042  mapdom2  7048  mapdom3  7049  phplem4  7059  php3  7063  sucdom2  7073  fineqvlem  7093  pssnn  7097  ssfi  7099  domfi  7100  findcard2  7114  ac6sfi  7117  isfinite2  7131  xpfi  7144  domunfican  7145  fiint  7149  fodomfib  7152  fissuni  7176  fipreima  7177  indexfi  7179  marypha1lem  7202  ordiso  7247  hartogslem1  7273  brwdom2  7303  wdomtr  7305  brwdom3  7312  unwdomg  7314  xpwdomg  7315  unxpwdom2  7318  unxpwdom  7319  inf3lem2  7346  infdifsn  7373  epfrs  7429  tcmin  7442  cplem1  7575  isinffi  7641  pm54.43  7649  dfac8alem  7672  dfac8b  7674  dfac8clem  7675  ac10ct  7677  ac5num  7679  acni2  7689  numacn  7692  acndom  7694  acndom2  7697  fodomacn  7699  numwdom  7702  wdomfil  7704  wdomnumr  7707  iunfictbso  7757  dfac2  7773  dfac9  7778  kmlem13  7804  cdainf  7834  infpss  7859  fictb  7887  cfeq0  7898  cff1  7900  cfflb  7901  cofsmo  7911  cfsmolem  7912  coftr  7915  infpssr  7950  fin4en1  7951  ssfin4  7952  domfin4  7953  fin23lem7  7958  enfin2i  7963  fin23lem31  7985  fin23lem41  7994  isf34lem4  8019  axcc3  8080  domtriomlem  8084  axdc2lem  8090  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  axcclem  8099  ac6num  8122  ttukeylem6  8157  ttukeyg  8160  fodomb  8167  iundom2g  8178  alephreg  8220  fpwwe2lem11  8278  fpwwe2lem12  8279  canthp1lem1  8290  canthp1  8292  pwfseq  8302  winafp  8335  wun0  8356  gruen  8450  grudomon  8455  gruina  8456  grur1  8458  ltexnq  8615  ltbtwnnq  8618  genpn0  8643  psslinpr  8671  prlem934  8673  ltaddpr  8674  ltexprlem2  8677  ltexprlem6  8681  ltexprlem7  8682  prlem936  8687  reclem2pr  8688  reclem4pr  8690  suplem1pr  8692  sup2  9726  supmul1  9735  supmul  9738  infmrcl  9749  negn0  10320  zsupss  10323  supxrre  10662  infmxrre  10670  ixxub  10693  ixxlb  10694  hashfun  11405  hashf1  11411  rlimdm  12041  climcau  12160  caucvgb  12168  summolem2  12205  zsum  12207  sumz  12211  fsumf1o  12212  fsumss  12214  fsumcl2lem  12220  fsumadd  12227  fsummulc2  12262  fsumconst  12268  fsumrelem  12281  isumltss  12323  ruclem13  12536  eulerth  12867  4sqlem12  13019  vdwapun  13037  vdwlem9  13052  vdwlem10  13053  ramub2  13077  ramz  13088  ramub1  13091  firest  13353  mremre  13522  isacs2  13571  iscatd2  13599  sscfn1  13710  sscfn2  13711  gsumval2a  14475  issubg2  14652  sylow1lem4  14928  sylow3  14960  prmcyg  15196  cyggex2  15199  gsumval3  15207  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumconst  15225  gsumzmhm  15226  gsumzoppg  15232  gsum2d2  15241  pgpfac1lem5  15330  ablfaclem3  15338  lss0cl  15720  lbspss  15851  lsmcv  15910  lspsnat  15914  cnsubrg  16448  gsumfsum  16455  cygzn  16540  obslbs  16646  eltg3  16716  tgtop  16727  tgidm  16734  ppttop  16760  toponmre  16846  tgrest  16906  tgcn  16998  lmff  17045  cmpsublem  17142  cmpsub  17143  tgcmp  17144  hauscmplem  17149  iunconlem  17169  uncon  17171  clscon  17172  1stcfb  17187  2ndcctbss  17197  2ndcdisj  17198  2ndcsep  17201  1stcelcls  17203  1stccnp  17204  1stckgen  17265  ptuni2  17287  ptbasfi  17292  ptpjopn  17322  ptclsg  17325  ptcnplem  17331  ptcnp  17332  txcn  17336  prdstopn  17338  txindis  17344  txtube  17350  txcmplem1  17351  txcmplem2  17352  xkococnlem  17369  txcon  17399  fbdmn0  17545  trfbas2  17554  filtop  17566  filcon  17594  filssufilg  17622  fmfnfm  17669  ufldom  17673  hauspwpwf1  17698  alexsubALTlem3  17759  alexsubALT  17761  ptcmplem2  17763  ptcmplem3  17764  tmdgsum2  17795  tgptsmscld  17849  tsmsxplem1  17851  xbln0  17981  met2ndci  18084  nmoid  18267  opnreen  18352  metdsre  18373  cnheibor  18469  phtpcer  18509  phtpc01  18510  phtpcco2  18513  cfilfcls  18716  cmetcaulem  18730  cmetcau  18731  iscmet3lem2  18734  iscmet3  18735  bcthlem4  18765  bcthlem5  18766  ovolctb  18865  ovoliunlem3  18879  ovoliunnul  18882  ovolicc2lem2  18893  ovolicc2lem5  18896  ovolicc2  18897  dyadmbl  18971  vitali  18984  mbfimaopnlem  19026  itg11  19062  bddmulibl  19209  limciun  19260  perfdvf  19269  dvcnp2  19285  dvlip  19356  dvne0  19374  fta1g  19569  fta1  19704  vieta1lem2  19707  ulmcau  19788  pserulm  19814  wilthlem2  20323  dchrvmasumif  20668  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem3  20684  dchrisum0  20685  dchrmusum  20689  dchrvmasum  20690  isgrp2d  20918  minvecolem5  21476  spansncvi  22247  esumcst  23451  derangenlem  23717  erdsze2lem1  23749  erdsze2  23751  ptpcon  23779  cvmsss2  23820  cvmopnlem  23824  cvmfolem  23825  cvmliftmolem2  23828  cvmliftlem15  23844  cvmlift2lem10  23858  cvmliftpht  23864  cvmlift3lem8  23872  rtrclreclem.trans  24058  prodmolem2  24158  zprod  24160  prod1  24169  fprodf1o  24172  fundmpss  24193  frmin  24313  wfrlem12  24338  frrlem11  24364  nocvxmin  24416  axcontlem10  24673  supaddc  24995  itg2addnclem  25003  injrec2  25222  surjsec2  25223  dffprod  25422  fnessref  26396  refssfne  26397  locfincmp  26407  comppfsc  26410  neibastop2lem  26412  neibastop2  26413  fnemeet2  26419  fnejoin2  26421  tailfb  26429  filnetlem3  26432  sdclem1  26556  fdc  26558  istotbnd3  26598  sstotbnd2  26601  sstotbnd  26602  prdsbnd  26620  prdstotbnd  26621  prdsbnd2  26622  heibor1lem  26636  heiborlem1  26638  heiborlem10  26647  heibor  26648  bfp  26651  riscer  26722  divrngidl  26756  prtlem17  26847  eldioph2lem1  26942  eldioph2lem2  26943  rencldnfilem  27006  kelac1  27264  enfixsn  27360  mapfien2  27361  lmiclbs  27410  lbslcic  27414  lmisfree  27415  hbt  27437  symggen  27514  psgnunilem3  27522  cncmpmax  27806  stoweidlem28  27880  stoweidlem31  27883  stoweidlem43  27895  stoweidlem46  27898  stoweidlem48  27900  stoweidlem56  27908  stoweidlem57  27909  stoweidlem59  27911  stoweidlem60  27912  rlimdmafv  28145  mpt2xopynvov0g  28196  frgra3vlem2  28425  onfrALT  28613  chordthmALT  29026  bnj849  29273  ax10NEW7  29450  ax11v2NEW7  29505  llnn0  30327  lplnn0N  30358  lvoln0N  30402  osumcllem8N  30774  pexmidlem5N  30785  diaglbN  31867  diaintclN  31870  dibglbN  31978  dibintclN  31979  dihglblem2aN  32105  dihintcl  32156  dvh1dim  32254  mapdrvallem2  32457
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator