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  4494  rexxfrd  4495  fvelimab  5614  foco2  5797  elunirn  5810  f1elima  5817  mpoexw  6268  tfrlem5  6369  tfrlemibacc  6381  tfrlemibfn  6383  tfr1onlembacc  6397  tfr1onlembfn  6399  tfrcllembacc  6410  tfrcllembfn  6412  frecabcl  6454  nnaordex  6583  nnawordex  6584  ectocld  6657  phpm  6923  dif1enen  6938  fin0  6943  fin0or  6944  fimax2gtri  6959  fidcenum  7017  suplub2ti  7062  supisoex  7070  enomnilem  7199  finomni  7201  enmkvlem  7222  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  ltexnqq  7470  ltbtwnnqq  7477  prarloclem4  7560  prarloc2  7566  genprndl  7583  genprndu  7584  prmuloc2  7629  1idprl  7652  1idpru  7653  cauappcvgprlemdisj  7713  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  recexgt0sr  7835  map2psrprg  7867  suplocsrlem  7870  nntopi  7956  cnegexlem1  8196  cnegexlem2  8197  renegcl  8282  aptap  8671  supinfneg  9663  infsupneg  9664  qmulz  9691  elpq  9717  icc0r  9995  exbtwnzlemstep  10319  rebtwn2zlemstep  10324  ioo0  10331  ico0  10333  ioc0  10334  modqmuladd  10440  addmodlteq  10472  frec2uzrand  10479  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  hashunlem  10878  shftlem  10963  caucvgre  11128  resqrexlemgt0  11167  rexico  11368  negfi  11374  climuni  11439  climshftlemg  11448  climcn1  11454  serf0  11498  summodclem2  11528  zsumdc  11530  fsum2dlemstep  11580  mertenslem2  11682  ntrivcvgap  11694  zproddc  11725  fprod2dlemstep  11768  dvds1lem  11948  odd2np1lem  12016  odd2np1  12017  sqoddm1div8z  12030  ltoddhalfle  12037  halfleoddlt  12038  m1expo  12044  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  flodddiv4  12078  bezoutlemaz  12143  bezoutlembz  12144  dvdssqim  12164  ncoprmgcdne1b  12230  coprmdvds2  12234  divgcdcoprm0  12242  cncongr1  12244  cncongr2  12245  dvdsnprmd  12266  rpexp  12294  pythagtriplem1  12406  pc2dvds  12471  difsqpwdvds  12479  oddprmdvds  12495  prmpwdvds  12496  4sqlem11  12542  dfgrp3mlem  13173  imasgrp2  13183  issubg4m  13266  imasabl  13409  ringinvnzdiv  13549  imasring  13563  dvdsrcl2  13598  dvdsrmul1  13601  isnzr2  13683  lss1d  13882  lssats2  13913  lspsn  13915  dvdsrzring  14102  znunit  14158  znrrg  14159  tgcl  14243  innei  14342  cnptoprest  14418  lmss  14425  lmtopcnp  14429  txlm  14458  blssps  14606  blss  14607  blssexps  14608  blssex  14609  mopni3  14663  metrest  14685  metcnp3  14690  mulc1cncf  14768  cncfco  14770  elply2  14914  gausslemma2dlem1a  15215  lgsquadlem1  15234  2lgsoddprmlem2  15263  subctctexmid  15561