Theorem rexlimdva 2477

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

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1433   E.wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353  df-rex 2354

This theorem is referenced by:  rexlimdvaa  2478  rexlimivv  2482  rexlimdvv  2483  ralxfrd  4212  rexxfrd  4213  fvelimab  5250  foco2  5339  elunirn  5426  f1elima  5433  tfrlem5  5953  tfrlemibacc  5963  tfrlemibfn  5965  nnaordex  6123  nnawordex  6124  ectocld  6195  phpm  6351  fin0  6369  fin0or  6370  suplub2ti  6414  supisoex  6422  ltexnqq  6598  ltbtwnnqq  6605  prarloclem4  6688  prarloc2  6694  genprndl  6711  genprndu  6712  prmuloc2  6757  1idprl  6780  1idpru  6781  cauappcvgprlemdisj  6841  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemladdrl  6868  recexgt0sr  6950  nntopi  7060  cnegexlem1  7283  cnegexlem2  7284  renegcl  7369  supinfneg  8683  infsupneg  8684  qmulz  8708  icc0r  8949  qbtwnzlemstep  9257  rebtwn2zlemstep  9261  ioo0  9268  ico0  9270  ioc0  9271  modqmuladd  9368  addmodlteq  9400  frec2uzrand  9407  frecuzrdgfn  9414  shftlem  9704  caucvgre  9867  resqrexlemgt0  9906  rexico  10107  negfi  10110  climuni  10132  climshftlemg  10141  climcn1  10147  serif0  10189  dvds1lem  10206  odd2np1lem  10271  odd2np1  10272  sqoddm1div8z  10286  ltoddhalfle  10293  halfleoddlt  10294  m1expo  10300  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  flodddiv4  10334  bezoutlemaz  10392  bezoutlembz  10393  dvdssqim  10413  ncoprmgcdne1b  10471  coprmdvds2  10475  divgcdcoprm0  10483  cncongr1  10485  cncongr2  10486  dvdsnprmd  10507  rpexp  10532