Theorem rexlimdva 2648

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)

Hypothesis

Ref	Expression
rexlimdva.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )

Assertion

Ref	Expression
rexlimdva	|- ( ph -> ( E. x e. A ps -> ch ) )

Distinct variable groups:   ph, x   ch, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimdva

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	ex 115	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2647	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200   E.wrex 2509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  rexlimdvaa  2649  rexlimivv  2654  rexlimdvv  2655  ralxfrd  4557  rexxfrd  4558  fvelimab  5698  foco2  5889  elunirn  5902  f1elima  5909  mpoexw  6373  tfrlem5  6475  tfrlemibacc  6487  tfrlemibfn  6489  tfr1onlembacc  6503  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembfn  6518  frecabcl  6560  nnaordex  6691  nnawordex  6692  ectocld  6765  phpm  7047  dif1enen  7062  fin0  7067  fin0or  7068  fimax2gtri  7084  fidcenum  7146  suplub2ti  7191  supisoex  7199  enomnilem  7328  finomni  7330  enmkvlem  7351  exmidfodomrlemeldju  7400  exmidfodomrlemreseldju  7401  ltexnqq  7618  ltbtwnnqq  7625  prarloclem4  7708  prarloc2  7714  genprndl  7731  genprndu  7732  prmuloc2  7777  1idprl  7800  1idpru  7801  cauappcvgprlemdisj  7861  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  recexgt0sr  7983  map2psrprg  8015  suplocsrlem  8018  nntopi  8104  cnegexlem1  8344  cnegexlem2  8345  renegcl  8430  aptap  8820  supinfneg  9819  infsupneg  9820  qmulz  9847  elpq  9873  icc0r  10151  exbtwnzlemstep  10497  rebtwn2zlemstep  10502  ioo0  10509  ico0  10511  ioc0  10512  modqmuladd  10618  addmodlteq  10650  frec2uzrand  10657  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  hashunlem  11057  reuccatpfxs1lem  11317  shftlem  11367  caucvgre  11532  resqrexlemgt0  11571  rexico  11772  negfi  11779  climuni  11844  climshftlemg  11853  climcn1  11859  serf0  11903  summodclem2  11933  zsumdc  11935  fsum2dlemstep  11985  mertenslem2  12087  ntrivcvgap  12099  zproddc  12130  fprod2dlemstep  12173  dvds1lem  12353  odd2np1lem  12423  odd2np1  12424  sqoddm1div8z  12437  ltoddhalfle  12444  halfleoddlt  12445  m1expo  12451  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  flodddiv4  12487  bezoutlemaz  12564  bezoutlembz  12565  dvdssqim  12585  ncoprmgcdne1b  12651  coprmdvds2  12655  divgcdcoprm0  12663  cncongr1  12665  cncongr2  12666  dvdsnprmd  12687  rpexp  12715  pythagtriplem1  12828  pc2dvds  12893  difsqpwdvds  12901  oddprmdvds  12917  prmpwdvds  12918  4sqlem11  12964  imasmnd2  13525  dfgrp3mlem  13671  imasgrp2  13687  issubg4m  13770  imasabl  13913  ringinvnzdiv  14053  imasring  14067  dvdsrcl2  14103  dvdsrmul1  14106  isnzr2  14188  lss1d  14387  lssats2  14418  lspsn  14420  dvdsrzring  14607  znunit  14663  znrrg  14664  tgcl  14778  innei  14877  cnptoprest  14953  lmss  14960  lmtopcnp  14964  txlm  14993  blssps  15141  blss  15142  blssexps  15143  blssex  15144  mopni3  15198  metrest  15220  metcnp3  15225  mulc1cncf  15303  cncfco  15305  elply2  15449  gausslemma2dlem1a  15777  lgsquadlem1  15796  2lgsoddprmlem2  15825  pw1ndom3  16525  subctctexmid  16537