Theorem rexlimdva 2650

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 2649	1 |- ( ph -> ( E. x e. A ps -> ch ) )

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  rexlimdvaa  2651  rexlimivv  2656  rexlimdvv  2657  ralxfrd  4559  rexxfrd  4560  fvelimab  5702  foco2  5893  elunirn  5906  f1elima  5913  mpoexw  6377  tfrlem5  6479  tfrlemibacc  6491  tfrlemibfn  6493  tfr1onlembacc  6507  tfr1onlembfn  6509  tfrcllembacc  6520  tfrcllembfn  6522  frecabcl  6564  nnaordex  6695  nnawordex  6696  ectocld  6769  phpm  7051  dif1enen  7068  fin0  7073  fin0or  7074  fimax2gtri  7090  fidcenum  7154  suplub2ti  7199  supisoex  7207  enomnilem  7336  finomni  7338  enmkvlem  7359  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  ltexnqq  7627  ltbtwnnqq  7634  prarloclem4  7717  prarloc2  7723  genprndl  7740  genprndu  7741  prmuloc2  7786  1idprl  7809  1idpru  7810  cauappcvgprlemdisj  7870  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  recexgt0sr  7992  map2psrprg  8024  suplocsrlem  8027  nntopi  8113  cnegexlem1  8353  cnegexlem2  8354  renegcl  8439  aptap  8829  supinfneg  9828  infsupneg  9829  qmulz  9856  elpq  9882  icc0r  10160  exbtwnzlemstep  10506  rebtwn2zlemstep  10511  ioo0  10518  ico0  10520  ioc0  10521  modqmuladd  10627  addmodlteq  10659  frec2uzrand  10666  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  hashunlem  11066  reuccatpfxs1lem  11326  shftlem  11376  caucvgre  11541  resqrexlemgt0  11580  rexico  11781  negfi  11788  climuni  11853  climshftlemg  11862  climcn1  11868  serf0  11912  summodclem2  11942  zsumdc  11944  fsum2dlemstep  11994  mertenslem2  12096  ntrivcvgap  12108  zproddc  12139  fprod2dlemstep  12182  dvds1lem  12362  odd2np1lem  12432  odd2np1  12433  sqoddm1div8z  12446  ltoddhalfle  12453  halfleoddlt  12454  m1expo  12460  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  flodddiv4  12496  bezoutlemaz  12573  bezoutlembz  12574  dvdssqim  12594  ncoprmgcdne1b  12660  coprmdvds2  12664  divgcdcoprm0  12672  cncongr1  12674  cncongr2  12675  dvdsnprmd  12696  rpexp  12724  pythagtriplem1  12837  pc2dvds  12902  difsqpwdvds  12910  oddprmdvds  12926  prmpwdvds  12927  4sqlem11  12973  imasmnd2  13534  dfgrp3mlem  13680  imasgrp2  13696  issubg4m  13779  imasabl  13922  ringinvnzdiv  14062  imasring  14076  dvdsrcl2  14112  dvdsrmul1  14115  isnzr2  14197  lss1d  14396  lssats2  14427  lspsn  14429  dvdsrzring  14616  znunit  14672  znrrg  14673  tgcl  14787  innei  14886  cnptoprest  14962  lmss  14969  lmtopcnp  14973  txlm  15002  blssps  15150  blss  15151  blssexps  15152  blssex  15153  mopni3  15207  metrest  15229  metcnp3  15234  mulc1cncf  15312  cncfco  15314  elply2  15458  gausslemma2dlem1a  15786  lgsquadlem1  15805  2lgsoddprmlem2  15834  uhgrspansubgrlem  16126  pw1ndom3  16589  subctctexmid  16601