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  5894  elunirn  5907  f1elima  5914  mpoexw  6378  tfrlem5  6480  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  frecabcl  6565  nnaordex  6696  nnawordex  6697  ectocld  6770  phpm  7052  dif1enen  7069  fin0  7074  fin0or  7075  fimax2gtri  7091  fidcenum  7155  suplub2ti  7200  supisoex  7208  enomnilem  7337  finomni  7339  enmkvlem  7360  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  ltexnqq  7628  ltbtwnnqq  7635  prarloclem4  7718  prarloc2  7724  genprndl  7741  genprndu  7742  prmuloc2  7787  1idprl  7810  1idpru  7811  cauappcvgprlemdisj  7871  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  recexgt0sr  7993  map2psrprg  8025  suplocsrlem  8028  nntopi  8114  cnegexlem1  8354  cnegexlem2  8355  renegcl  8440  aptap  8830  supinfneg  9829  infsupneg  9830  qmulz  9857  elpq  9883  icc0r  10161  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  ioo0  10520  ico0  10522  ioc0  10523  modqmuladd  10629  addmodlteq  10661  frec2uzrand  10668  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  hashunlem  11068  reuccatpfxs1lem  11331  shftlem  11394  caucvgre  11559  resqrexlemgt0  11598  rexico  11799  negfi  11806  climuni  11871  climshftlemg  11880  climcn1  11886  serf0  11930  summodclem2  11961  zsumdc  11963  fsum2dlemstep  12013  mertenslem2  12115  ntrivcvgap  12127  zproddc  12158  fprod2dlemstep  12201  dvds1lem  12381  odd2np1lem  12451  odd2np1  12452  sqoddm1div8z  12465  ltoddhalfle  12472  halfleoddlt  12473  m1expo  12479  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  flodddiv4  12515  bezoutlemaz  12592  bezoutlembz  12593  dvdssqim  12613  ncoprmgcdne1b  12679  coprmdvds2  12683  divgcdcoprm0  12691  cncongr1  12693  cncongr2  12694  dvdsnprmd  12715  rpexp  12743  pythagtriplem1  12856  pc2dvds  12921  difsqpwdvds  12929  oddprmdvds  12945  prmpwdvds  12946  4sqlem11  12992  imasmnd2  13553  dfgrp3mlem  13699  imasgrp2  13715  issubg4m  13798  imasabl  13941  ringinvnzdiv  14082  imasring  14096  dvdsrcl2  14132  dvdsrmul1  14135  isnzr2  14217  lss1d  14416  lssats2  14447  lspsn  14449  dvdsrzring  14636  znunit  14692  znrrg  14693  tgcl  14807  innei  14906  cnptoprest  14982  lmss  14989  lmtopcnp  14993  txlm  15022  blssps  15170  blss  15171  blssexps  15172  blssex  15173  mopni3  15227  metrest  15249  metcnp3  15254  mulc1cncf  15332  cncfco  15334  elply2  15478  gausslemma2dlem1a  15806  lgsquadlem1  15825  2lgsoddprmlem2  15854  uhgrspansubgrlem  16146  pw1ndom3  16640  subctctexmid  16652