Theorem rexlimdva 2611

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  rexlimdvaa  2612  rexlimivv  2617  rexlimdvv  2618  ralxfrd  4493  rexxfrd  4494  fvelimab  5613  foco2  5796  elunirn  5809  f1elima  5816  mpoexw  6266  tfrlem5  6367  tfrlemibacc  6379  tfrlemibfn  6381  tfr1onlembacc  6395  tfr1onlembfn  6397  tfrcllembacc  6408  tfrcllembfn  6410  frecabcl  6452  nnaordex  6581  nnawordex  6582  ectocld  6655  phpm  6921  dif1enen  6936  fin0  6941  fin0or  6942  fimax2gtri  6957  fidcenum  7015  suplub2ti  7060  supisoex  7068  enomnilem  7197  finomni  7199  enmkvlem  7220  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  ltexnqq  7468  ltbtwnnqq  7475  prarloclem4  7558  prarloc2  7564  genprndl  7581  genprndu  7582  prmuloc2  7627  1idprl  7650  1idpru  7651  cauappcvgprlemdisj  7711  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemladdrl  7738  recexgt0sr  7833  map2psrprg  7865  suplocsrlem  7868  nntopi  7954  cnegexlem1  8194  cnegexlem2  8195  renegcl  8280  aptap  8669  supinfneg  9660  infsupneg  9661  qmulz  9688  elpq  9714  icc0r  9992  exbtwnzlemstep  10316  rebtwn2zlemstep  10321  ioo0  10328  ico0  10330  ioc0  10331  modqmuladd  10437  addmodlteq  10469  frec2uzrand  10476  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  hashunlem  10875  shftlem  10960  caucvgre  11125  resqrexlemgt0  11164  rexico  11365  negfi  11371  climuni  11436  climshftlemg  11445  climcn1  11451  serf0  11495  summodclem2  11525  zsumdc  11527  fsum2dlemstep  11577  mertenslem2  11679  ntrivcvgap  11691  zproddc  11722  fprod2dlemstep  11765  dvds1lem  11945  odd2np1lem  12013  odd2np1  12014  sqoddm1div8z  12027  ltoddhalfle  12034  halfleoddlt  12035  m1expo  12041  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  flodddiv4  12075  bezoutlemaz  12140  bezoutlembz  12141  dvdssqim  12161  ncoprmgcdne1b  12227  coprmdvds2  12231  divgcdcoprm0  12239  cncongr1  12241  cncongr2  12242  dvdsnprmd  12263  rpexp  12291  pythagtriplem1  12403  pc2dvds  12468  difsqpwdvds  12476  oddprmdvds  12492  prmpwdvds  12493  4sqlem11  12539  dfgrp3mlem  13170  imasgrp2  13180  issubg4m  13263  imasabl  13406  ringinvnzdiv  13546  imasring  13560  dvdsrcl2  13595  dvdsrmul1  13598  isnzr2  13680  lss1d  13879  lssats2  13910  lspsn  13912  dvdsrzring  14091  znunit  14147  znrrg  14148  tgcl  14232  innei  14331  cnptoprest  14407  lmss  14414  lmtopcnp  14418  txlm  14447  blssps  14595  blss  14596  blssexps  14597  blssex  14598  mopni3  14652  metrest  14674  metcnp3  14679  mulc1cncf  14744  cncfco  14746  elply2  14881  gausslemma2dlem1a  15174  lgsquadlem1  15191  2lgsoddprmlem2  15194  subctctexmid  15491