Theorem rexlimdva 2662

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

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

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 2527  df-rex 2528

This theorem is referenced by:  rexlimdvaa  2663  rexlimivv  2668  rexlimdvv  2669  ralxfrd  4588  rexxfrd  4589  fvelimab  5738  foco2  5932  elunirn  5945  f1elima  5952  mpoexw  6422  tfrlem5  6558  tfrlemibacc  6570  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembfn  6601  frecabcl  6643  nnaordex  6774  nnawordex  6775  ectocld  6848  phpm  7133  dif1enen  7150  fin0  7155  fin0or  7156  fimax2gtri  7172  fidcenum  7239  suplub2ti  7305  supisoex  7313  enomnilem  7442  finomni  7444  enmkvlem  7465  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  ltexnqq  7739  ltbtwnnqq  7746  prarloclem4  7829  prarloc2  7835  genprndl  7852  genprndu  7853  prmuloc2  7898  1idprl  7921  1idpru  7922  cauappcvgprlemdisj  7982  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  recexgt0sr  8104  map2psrprg  8136  suplocsrlem  8139  nntopi  8225  cnegexlem1  8464  cnegexlem2  8465  renegcl  8550  aptap  8941  supinfneg  9945  infsupneg  9946  qmulz  9973  elpq  9999  icc0r  10278  exbtwnzlemstep  10631  rebtwn2zlemstep  10636  ioo0  10643  ico0  10645  ioc0  10646  modqmuladd  10752  addmodlteq  10784  frec2uzrand  10791  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  hashunlem  11193  reuccatpfxs1lem  11463  shftlem  11526  caucvgre  11691  resqrexlemgt0  11730  rexico  11931  negfi  11938  climuni  12003  climshftlemg  12012  climcn1  12018  serf0  12062  summodclem2  12093  zsumdc  12095  fsum2dlemstep  12145  mertenslem2  12247  ntrivcvgap  12259  zproddc  12290  fprod2dlemstep  12333  dvds1lem  12513  odd2np1lem  12583  odd2np1  12584  sqoddm1div8z  12597  ltoddhalfle  12604  halfleoddlt  12605  m1expo  12611  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  flodddiv4  12647  bezoutlemaz  12724  bezoutlembz  12725  dvdssqim  12745  ncoprmgcdne1b  12811  coprmdvds2  12815  divgcdcoprm0  12823  cncongr1  12825  cncongr2  12826  dvdsnprmd  12847  rpexp  12875  pythagtriplem1  12988  pc2dvds  13053  difsqpwdvds  13061  oddprmdvds  13077  prmpwdvds  13078  4sqlem11  13124  imasmnd2  13707  dfgrp3mlem  13853  imasgrp2  13863  issubg4m  13946  imasabl  14089  ringinvnzdiv  14293  imasring  14307  dvdsrcl2  14344  dvdsrmul1  14347  isnzr2  14429  lss1d  14657  lssats2  14688  lspsn  14690  dvdsrzring  14877  znunit  14933  znrrg  14934  tgcl  15055  innei  15154  cnptoprest  15230  lmss  15237  lmtopcnp  15241  txlm  15270  blssps  15418  blss  15419  blssexps  15420  blssex  15421  mopni3  15475  metrest  15497  metcnp3  15502  mulc1cncf  15580  cncfco  15582  elply2  15726  gausslemma2dlem1a  16057  lgsquadlem1  16076  2lgsoddprmlem2  16105  uhgrspansubgrlem  16397  pw1ndom3  16890  subctctexmid  16900