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

Theorem exlimdv 1933
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
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 nfv 1629 . 2  |-  F/ x ph
2 nfv 1629 . 2  |-  F/ x ch
3 exlimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3exlimd 1784 1  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537
This theorem is referenced by:  ax11v2  1936  ax11v2-o  1937  exlimdvv  2027  ax11eq  2108  ax11el  2109  ax11inda  2116  tpid3g  3701  sssn  3732  euotd  4225  wefrc  4345  wereu2  4348  onfr  4389  reusv2lem2  4494  ralxfr2d  4508  releldmb  4887  relelrnb  4888  elres  4964  iss  4972  soex  5096  dffv2  5512  fvmptdv2  5533  dff3  5593  elunirnALT  5699  isomin  5754  isofrlem  5757  f1oweALT  5771  ovmpt4g  5890  op1steq  6084  reldmtpos  6162  rntpos  6167  tfrlem9a  6356  erref  6634  erdisj  6661  map0g  6761  resixpfo  6808  domdifsn  6899  xpdom2  6911  xpdom3  6914  domunsncan  6916  domunsn  6965  fodomr  6966  mapdom1  6980  mapdom2  6986  mapdom3  6987  phplem4  6997  php3  7001  sucdom2  7011  fineqvlem  7031  pssnn  7035  ssfi  7037  domfi  7038  findcard2  7052  ac6sfi  7055  isfinite2  7069  xpfi  7082  domunfican  7083  fiint  7087  fodomfib  7090  fissuni  7114  fipreima  7115  indexfi  7117  marypha1lem  7140  ordiso  7185  hartogslem1  7211  brwdom2  7241  wdomtr  7243  brwdom3  7250  unwdomg  7252  xpwdomg  7253  unxpwdom2  7256  unxpwdom  7257  inf3lem2  7284  infdifsn  7311  epfrs  7367  tcmin  7380  cplem1  7513  isinffi  7579  pm54.43  7587  dfac8alem  7610  dfac8b  7612  dfac8clem  7613  ac10ct  7615  ac5num  7617  acni2  7627  numacn  7630  acndom  7632  acndom2  7635  fodomacn  7637  numwdom  7640  wdomfil  7642  wdomnumr  7645  iunfictbso  7695  dfac2  7711  dfac9  7716  kmlem13  7742  cdainf  7772  infpss  7797  fictb  7825  cfeq0  7836  cff1  7838  cfflb  7839  cofsmo  7849  cfsmolem  7850  coftr  7853  infpssr  7888  fin4en1  7889  ssfin4  7890  domfin4  7891  fin23lem7  7896  enfin2i  7901  fin23lem31  7923  fin23lem41  7932  isf34lem4  7957  axcc3  8018  domtriomlem  8022  axdc2lem  8028  axdc3lem2  8031  axdc3lem4  8033  axdc4lem  8035  axcclem  8037  ac6num  8060  ttukeylem6  8095  ttukeyg  8098  fodomb  8105  iundom2g  8116  alephreg  8158  fpwwe2lem11  8216  fpwwe2lem12  8217  canthp1lem1  8228  canthp1  8230  pwfseq  8240  winafp  8273  wun0  8294  gruen  8388  grudomon  8393  gruina  8394  grur1  8396  ltexnq  8553  ltbtwnnq  8556  genpn0  8581  psslinpr  8609  prlem934  8611  ltaddpr  8612  ltexprlem2  8615  ltexprlem6  8619  ltexprlem7  8620  prlem936  8625  reclem2pr  8626  reclem4pr  8628  suplem1pr  8630  sup2  9664  supmul1  9673  supmul  9676  infmrcl  9687  negn0  10257  zsupss  10260  supxrre  10598  infmxrre  10606  ixxub  10629  ixxlb  10630  hashfun  11340  hashf1  11346  rlimdm  11976  climcau  12095  caucvgb  12103  summolem2  12140  zsum  12142  sumz  12146  fsumf1o  12147  fsumss  12149  fsumcl2lem  12155  fsumadd  12162  fsummulc2  12197  fsumconst  12203  fsumrelem  12216  isumltss  12255  ruclem13  12468  eulerth  12799  4sqlem12  12951  vdwapun  12969  vdwlem9  12984  vdwlem10  12985  ramub2  13009  ramz  13020  ramub1  13023  firest  13285  mremre  13454  isacs2  13503  iscatd2  13531  sscfn1  13642  sscfn2  13643  gsumval2a  14407  issubg2  14584  sylow1lem4  14860  sylow3  14892  prmcyg  15128  cyggex2  15131  gsumval3  15139  gsumzres  15142  gsumzcl  15143  gsumzf1o  15144  gsumzaddlem  15151  gsumconst  15157  gsumzmhm  15158  gsumzoppg  15164  gsum2d2  15173  pgpfac1lem5  15262  ablfaclem3  15270  lss0cl  15652  lbspss  15783  lsmcv  15842  lspsnat  15846  cnsubrg  16380  gsumfsum  16387  cygzn  16472  obslbs  16578  eltg3  16648  tgtop  16659  tgidm  16666  ppttop  16692  toponmre  16778  tgrest  16838  tgcn  16930  lmff  16977  cmpsublem  17074  cmpsub  17075  tgcmp  17076  hauscmplem  17081  iunconlem  17101  uncon  17103  clscon  17104  1stcfb  17119  2ndcctbss  17129  2ndcdisj  17130  2ndcsep  17133  1stcelcls  17135  1stccnp  17136  1stckgen  17197  ptuni2  17219  ptbasfi  17224  ptpjopn  17254  ptclsg  17257  ptcnplem  17263  ptcnp  17264  txcn  17268  prdstopn  17270  txindis  17276  txtube  17282  txcmplem1  17283  txcmplem2  17284  xkococnlem  17301  txcon  17331  fbdmn0  17477  trfbas2  17486  filtop  17498  filcon  17526  filssufilg  17554  fmfnfm  17601  ufldom  17605  hauspwpwf1  17630  alexsubALTlem3  17691  alexsubALT  17693  ptcmplem2  17695  ptcmplem3  17696  tmdgsum2  17727  tgptsmscld  17781  tsmsxplem1  17783  xbln0  17913  met2ndci  18016  nmoid  18199  opnreen  18284  metdsre  18305  cnheibor  18401  phtpcer  18441  phtpc01  18442  phtpcco2  18445  cfilfcls  18648  cmetcaulem  18662  cmetcau  18663  iscmet3lem2  18666  iscmet3  18667  bcthlem4  18697  bcthlem5  18698  ovolctb  18797  ovoliunlem3  18811  ovoliunnul  18814  ovolicc2lem2  18825  ovolicc2lem5  18828  ovolicc2  18829  dyadmbl  18903  vitali  18916  mbfimaopnlem  18958  itg11  18994  bddmulibl  19141  limciun  19192  perfdvf  19201  dvcnp2  19217  dvlip  19288  dvne0  19306  fta1g  19501  fta1  19636  vieta1lem2  19639  ulmcau  19720  pserulm  19746  wilthlem2  20255  dchrvmasumif  20600  rpvmasum2  20609  dchrisum0re  20610  dchrisum0lem3  20616  dchrisum0  20617  dchrmusum  20621  dchrvmasum  20622  isgrp2d  20848  minvecolem5  21406  spansncvi  22195  derangenlem  23060  erdsze2lem1  23092  erdsze2  23094  ptpcon  23122  cvmsss2  23163  cvmopnlem  23167  cvmfolem  23168  cvmliftmolem2  23171  cvmliftlem15  23187  cvmlift2lem10  23201  cvmliftpht  23207  cvmlift3lem8  23215  rtrclreclem.trans  23401  fundmpss  23477  frmin  23597  wfrlem12  23622  frrlem11  23648  nocvxmin  23700  axcontlem10  23962  injrec2  24472  surjsec2  24473  dffprod  24672  fnessref  25646  refssfne  25647  locfincmp  25657  comppfsc  25660  neibastop2lem  25662  neibastop2  25663  fnemeet2  25669  fnejoin2  25671  tailfb  25679  filnetlem3  25682  sdclem1  25806  fdc  25808  istotbnd3  25848  sstotbnd2  25851  sstotbnd  25852  prdsbnd  25870  prdstotbnd  25871  prdsbnd2  25872  heibor1lem  25886  heiborlem1  25888  heiborlem10  25897  heibor  25898  bfp  25901  riscer  25972  divrngidl  26006  prtlem17  26097  eldioph2lem1  26192  eldioph2lem2  26193  rencldnfilem  26256  kelac1  26514  enfixsn  26610  mapfien2  26611  lmiclbs  26660  lbslcic  26664  lmisfree  26665  hbt  26687  symggen  26764  psgnunilem3  26772  cncmpmax  27057  stoweidlem28  27098  stoweidlem31  27101  stoweidlem43  27113  stoweidlem46  27116  stoweidlem48  27118  stoweidlem56  27126  stoweidlem57  27127  stoweidlem59  27129  stoweidlem60  27130  onfrALT  27351  bnj849  27990  llnn0  28856  lplnn0N  28887  lvoln0N  28931  osumcllem8N  29303  pexmidlem5N  29314  diaglbN  30396  diaintclN  30399  dibglbN  30507  dibintclN  30508  dihglblem2aN  30634  dihintcl  30685  dvh1dim  30783  mapdrvallem2  30986
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator