Theorem rexlimdva 2582

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

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

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2448  df-rex 2449

This theorem is referenced by:  rexlimdvaa  2583  rexlimivv  2588  rexlimdvv  2589  ralxfrd  4439  rexxfrd  4440  fvelimab  5541  foco2  5721  elunirn  5733  f1elima  5740  tfrlem5  6278  tfrlemibacc  6290  tfrlemibfn  6292  tfr1onlembacc  6306  tfr1onlembfn  6308  tfrcllembacc  6319  tfrcllembfn  6321  frecabcl  6363  nnaordex  6491  nnawordex  6492  ectocld  6563  phpm  6827  dif1enen  6842  fin0  6847  fin0or  6848  fimax2gtri  6863  fidcenum  6917  suplub2ti  6962  supisoex  6970  enomnilem  7098  finomni  7100  enmkvlem  7121  exmidfodomrlemeldju  7151  exmidfodomrlemreseldju  7152  ltexnqq  7345  ltbtwnnqq  7352  prarloclem4  7435  prarloc2  7441  genprndl  7458  genprndu  7459  prmuloc2  7504  1idprl  7527  1idpru  7528  cauappcvgprlemdisj  7588  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  caucvgprlemladdrl  7615  recexgt0sr  7710  map2psrprg  7742  suplocsrlem  7745  nntopi  7831  cnegexlem1  8069  cnegexlem2  8070  renegcl  8155  supinfneg  9529  infsupneg  9530  qmulz  9557  elpq  9582  icc0r  9858  exbtwnzlemstep  10179  rebtwn2zlemstep  10184  ioo0  10191  ico0  10193  ioc0  10194  modqmuladd  10297  addmodlteq  10329  frec2uzrand  10336  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  hashunlem  10713  shftlem  10754  caucvgre  10919  resqrexlemgt0  10958  rexico  11159  negfi  11165  climuni  11230  climshftlemg  11239  climcn1  11245  serf0  11289  summodclem2  11319  zsumdc  11321  fsum2dlemstep  11371  mertenslem2  11473  ntrivcvgap  11485  zproddc  11516  fprod2dlemstep  11559  dvds1lem  11738  odd2np1lem  11805  odd2np1  11806  sqoddm1div8z  11819  ltoddhalfle  11826  halfleoddlt  11827  m1expo  11833  divalglemeunn  11854  divalglemex  11855  divalglemeuneg  11856  flodddiv4  11867  bezoutlemaz  11932  bezoutlembz  11933  dvdssqim  11953  ncoprmgcdne1b  12017  coprmdvds2  12021  divgcdcoprm0  12029  cncongr1  12031  cncongr2  12032  dvdsnprmd  12053  rpexp  12081  pythagtriplem1  12193  pc2dvds  12257  difsqpwdvds  12265  oddprmdvds  12280  prmpwdvds  12281  tgcl  12664  innei  12763  cnptoprest  12839  lmss  12846  lmtopcnp  12850  txlm  12879  blssps  13027  blss  13028  blssexps  13029  blssex  13030  mopni3  13084  metrest  13106  metcnp3  13111  mulc1cncf  13176  cncfco  13178  subctctexmid  13841