Theorem rexlimdva 2521

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-i5r 1496

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-ral 2393  df-rex 2394

This theorem is referenced by:  rexlimdvaa  2522  rexlimivv  2527  rexlimdvv  2528  ralxfrd  4341  rexxfrd  4342  fvelimab  5429  foco2  5607  elunirn  5619  f1elima  5626  tfrlem5  6163  tfrlemibacc  6175  tfrlemibfn  6177  tfr1onlembacc  6191  tfr1onlembfn  6193  tfrcllembacc  6204  tfrcllembfn  6206  frecabcl  6248  nnaordex  6375  nnawordex  6376  ectocld  6447  phpm  6710  dif1enen  6725  fin0  6730  fin0or  6731  fimax2gtri  6746  fidcenum  6794  suplub2ti  6838  supisoex  6846  enomnilem  6958  finomni  6960  exmidfodomrlemeldju  7000  exmidfodomrlemreseldju  7001  ltexnqq  7158  ltbtwnnqq  7165  prarloclem4  7248  prarloc2  7254  genprndl  7271  genprndu  7272  prmuloc2  7317  1idprl  7340  1idpru  7341  cauappcvgprlemdisj  7401  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  caucvgprlemladdrl  7428  recexgt0sr  7510  nntopi  7623  cnegexlem1  7854  cnegexlem2  7855  renegcl  7940  supinfneg  9286  infsupneg  9287  qmulz  9311  icc0r  9596  exbtwnzlemstep  9912  rebtwn2zlemstep  9917  ioo0  9924  ico0  9926  ioc0  9927  modqmuladd  10026  addmodlteq  10058  frec2uzrand  10065  frecuzrdgtcl  10072  frecuzrdgfunlem  10079  hashunlem  10437  shftlem  10475  caucvgre  10639  resqrexlemgt0  10678  rexico  10879  negfi  10885  climuni  10948  climshftlemg  10957  climcn1  10963  serf0  11007  summodclem2  11037  zsumdc  11039  fsum2dlemstep  11089  mertenslem2  11191  dvds1lem  11346  odd2np1lem  11411  odd2np1  11412  sqoddm1div8z  11425  ltoddhalfle  11432  halfleoddlt  11433  m1expo  11439  divalglemeunn  11460  divalglemex  11461  divalglemeuneg  11462  flodddiv4  11473  bezoutlemaz  11531  bezoutlembz  11532  dvdssqim  11552  ncoprmgcdne1b  11610  coprmdvds2  11614  divgcdcoprm0  11622  cncongr1  11624  cncongr2  11625  dvdsnprmd  11646  rpexp  11671  tgcl  12070  innei  12169  cnptoprest  12244  lmss  12251  lmtopcnp  12255  txlm  12284  blssps  12410  blss  12411  blssexps  12412  blssex  12413  mopni3  12467  metrest  12489  metcnp3  12494  mulc1cncf  12556  cncfco  12558