Theorem rexlimdva 2651

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  rexlimdvaa  2652  rexlimivv  2657  rexlimdvv  2658  ralxfrd  4565  rexxfrd  4566  fvelimab  5711  foco2  5904  elunirn  5917  f1elima  5924  mpoexw  6387  tfrlem5  6523  tfrlemibacc  6535  tfrlemibfn  6537  tfr1onlembacc  6551  tfr1onlembfn  6553  tfrcllembacc  6564  tfrcllembfn  6566  frecabcl  6608  nnaordex  6739  nnawordex  6740  ectocld  6813  phpm  7095  dif1enen  7112  fin0  7117  fin0or  7118  fimax2gtri  7134  fidcenum  7198  suplub2ti  7243  supisoex  7251  enomnilem  7380  finomni  7382  enmkvlem  7403  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  ltexnqq  7671  ltbtwnnqq  7678  prarloclem4  7761  prarloc2  7767  genprndl  7784  genprndu  7785  prmuloc2  7830  1idprl  7853  1idpru  7854  cauappcvgprlemdisj  7914  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  recexgt0sr  8036  map2psrprg  8068  suplocsrlem  8071  nntopi  8157  cnegexlem1  8396  cnegexlem2  8397  renegcl  8482  aptap  8872  supinfneg  9873  infsupneg  9874  qmulz  9901  elpq  9927  icc0r  10205  exbtwnzlemstep  10553  rebtwn2zlemstep  10558  ioo0  10565  ico0  10567  ioc0  10568  modqmuladd  10674  addmodlteq  10706  frec2uzrand  10713  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  hashunlem  11113  reuccatpfxs1lem  11376  shftlem  11439  caucvgre  11604  resqrexlemgt0  11643  rexico  11844  negfi  11851  climuni  11916  climshftlemg  11925  climcn1  11931  serf0  11975  summodclem2  12006  zsumdc  12008  fsum2dlemstep  12058  mertenslem2  12160  ntrivcvgap  12172  zproddc  12203  fprod2dlemstep  12246  dvds1lem  12426  odd2np1lem  12496  odd2np1  12497  sqoddm1div8z  12510  ltoddhalfle  12517  halfleoddlt  12518  m1expo  12524  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  flodddiv4  12560  bezoutlemaz  12637  bezoutlembz  12638  dvdssqim  12658  ncoprmgcdne1b  12724  coprmdvds2  12728  divgcdcoprm0  12736  cncongr1  12738  cncongr2  12739  dvdsnprmd  12760  rpexp  12788  pythagtriplem1  12901  pc2dvds  12966  difsqpwdvds  12974  oddprmdvds  12990  prmpwdvds  12991  4sqlem11  13037  imasmnd2  13598  dfgrp3mlem  13744  imasgrp2  13760  issubg4m  13843  imasabl  13986  ringinvnzdiv  14127  imasring  14141  dvdsrcl2  14177  dvdsrmul1  14180  isnzr2  14262  lss1d  14462  lssats2  14493  lspsn  14495  dvdsrzring  14682  znunit  14738  znrrg  14739  tgcl  14858  innei  14957  cnptoprest  15033  lmss  15040  lmtopcnp  15044  txlm  15073  blssps  15221  blss  15222  blssexps  15223  blssex  15224  mopni3  15278  metrest  15300  metcnp3  15305  mulc1cncf  15383  cncfco  15385  elply2  15529  gausslemma2dlem1a  15860  lgsquadlem1  15879  2lgsoddprmlem2  15908  uhgrspansubgrlem  16200  pw1ndom3  16693  subctctexmid  16705