Theorem rexlimdva 2625

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491  df-rex 2492

This theorem is referenced by:  rexlimdvaa  2626  rexlimivv  2631  rexlimdvv  2632  ralxfrd  4527  rexxfrd  4528  fvelimab  5658  foco2  5845  elunirn  5858  f1elima  5865  mpoexw  6322  tfrlem5  6423  tfrlemibacc  6435  tfrlemibfn  6437  tfr1onlembacc  6451  tfr1onlembfn  6453  tfrcllembacc  6464  tfrcllembfn  6466  frecabcl  6508  nnaordex  6637  nnawordex  6638  ectocld  6711  phpm  6988  dif1enen  7003  fin0  7008  fin0or  7009  fimax2gtri  7024  fidcenum  7084  suplub2ti  7129  supisoex  7137  enomnilem  7266  finomni  7268  enmkvlem  7289  exmidfodomrlemeldju  7338  exmidfodomrlemreseldju  7339  ltexnqq  7556  ltbtwnnqq  7563  prarloclem4  7646  prarloc2  7652  genprndl  7669  genprndu  7670  prmuloc2  7715  1idprl  7738  1idpru  7739  cauappcvgprlemdisj  7799  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprlemladdrl  7826  recexgt0sr  7921  map2psrprg  7953  suplocsrlem  7956  nntopi  8042  cnegexlem1  8282  cnegexlem2  8283  renegcl  8368  aptap  8758  supinfneg  9751  infsupneg  9752  qmulz  9779  elpq  9805  icc0r  10083  exbtwnzlemstep  10427  rebtwn2zlemstep  10432  ioo0  10439  ico0  10441  ioc0  10442  modqmuladd  10548  addmodlteq  10580  frec2uzrand  10587  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  hashunlem  10986  reuccatpfxs1lem  11237  shftlem  11242  caucvgre  11407  resqrexlemgt0  11446  rexico  11647  negfi  11654  climuni  11719  climshftlemg  11728  climcn1  11734  serf0  11778  summodclem2  11808  zsumdc  11810  fsum2dlemstep  11860  mertenslem2  11962  ntrivcvgap  11974  zproddc  12005  fprod2dlemstep  12048  dvds1lem  12228  odd2np1lem  12298  odd2np1  12299  sqoddm1div8z  12312  ltoddhalfle  12319  halfleoddlt  12320  m1expo  12326  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  flodddiv4  12362  bezoutlemaz  12439  bezoutlembz  12440  dvdssqim  12460  ncoprmgcdne1b  12526  coprmdvds2  12530  divgcdcoprm0  12538  cncongr1  12540  cncongr2  12541  dvdsnprmd  12562  rpexp  12590  pythagtriplem1  12703  pc2dvds  12768  difsqpwdvds  12776  oddprmdvds  12792  prmpwdvds  12793  4sqlem11  12839  imasmnd2  13399  dfgrp3mlem  13545  imasgrp2  13561  issubg4m  13644  imasabl  13787  ringinvnzdiv  13927  imasring  13941  dvdsrcl2  13976  dvdsrmul1  13979  isnzr2  14061  lss1d  14260  lssats2  14291  lspsn  14293  dvdsrzring  14480  znunit  14536  znrrg  14537  tgcl  14651  innei  14750  cnptoprest  14826  lmss  14833  lmtopcnp  14837  txlm  14866  blssps  15014  blss  15015  blssexps  15016  blssex  15017  mopni3  15071  metrest  15093  metcnp3  15098  mulc1cncf  15176  cncfco  15178  elply2  15322  gausslemma2dlem1a  15650  lgsquadlem1  15669  2lgsoddprmlem2  15698  subctctexmid  16139