Theorem rexlimdva 2574

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 114	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2573	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2128   E.wrex 2436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440  df-rex 2441

This theorem is referenced by:  rexlimdvaa  2575  rexlimivv  2580  rexlimdvv  2581  ralxfrd  4421  rexxfrd  4422  fvelimab  5523  foco2  5701  elunirn  5713  f1elima  5720  tfrlem5  6258  tfrlemibacc  6270  tfrlemibfn  6272  tfr1onlembacc  6286  tfr1onlembfn  6288  tfrcllembacc  6299  tfrcllembfn  6301  frecabcl  6343  nnaordex  6471  nnawordex  6472  ectocld  6543  phpm  6807  dif1enen  6822  fin0  6827  fin0or  6828  fimax2gtri  6843  fidcenum  6897  suplub2ti  6941  supisoex  6949  enomnilem  7075  finomni  7077  enmkvlem  7098  exmidfodomrlemeldju  7128  exmidfodomrlemreseldju  7129  ltexnqq  7322  ltbtwnnqq  7329  prarloclem4  7412  prarloc2  7418  genprndl  7435  genprndu  7436  prmuloc2  7481  1idprl  7504  1idpru  7505  cauappcvgprlemdisj  7565  cauappcvgprlemladdru  7570  cauappcvgprlemladdrl  7571  caucvgprlemladdrl  7592  recexgt0sr  7687  map2psrprg  7719  suplocsrlem  7722  nntopi  7808  cnegexlem1  8044  cnegexlem2  8045  renegcl  8130  supinfneg  9500  infsupneg  9501  qmulz  9525  elpq  9550  icc0r  9823  exbtwnzlemstep  10140  rebtwn2zlemstep  10145  ioo0  10152  ico0  10154  ioc0  10155  modqmuladd  10258  addmodlteq  10290  frec2uzrand  10297  frecuzrdgtcl  10304  frecuzrdgfunlem  10311  hashunlem  10671  shftlem  10709  caucvgre  10874  resqrexlemgt0  10913  rexico  11114  negfi  11120  climuni  11183  climshftlemg  11192  climcn1  11198  serf0  11242  summodclem2  11272  zsumdc  11274  fsum2dlemstep  11324  mertenslem2  11426  ntrivcvgap  11438  zproddc  11469  fprod2dlemstep  11512  dvds1lem  11690  odd2np1lem  11755  odd2np1  11756  sqoddm1div8z  11769  ltoddhalfle  11776  halfleoddlt  11777  m1expo  11783  divalglemeunn  11804  divalglemex  11805  divalglemeuneg  11806  flodddiv4  11817  bezoutlemaz  11878  bezoutlembz  11879  dvdssqim  11899  ncoprmgcdne1b  11957  coprmdvds2  11961  divgcdcoprm0  11969  cncongr1  11971  cncongr2  11972  dvdsnprmd  11993  rpexp  12018  tgcl  12435  innei  12534  cnptoprest  12610  lmss  12617  lmtopcnp  12621  txlm  12650  blssps  12798  blss  12799  blssexps  12800  blssex  12801  mopni3  12855  metrest  12877  metcnp3  12882  mulc1cncf  12947  cncfco  12949  subctctexmid  13544