Theorem rexlimdva 2648

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  rexlimdvaa  2649  rexlimivv  2654  rexlimdvv  2655  ralxfrd  4552  rexxfrd  4553  fvelimab  5689  foco2  5876  elunirn  5889  f1elima  5896  mpoexw  6357  tfrlem5  6458  tfrlemibacc  6470  tfrlemibfn  6472  tfr1onlembacc  6486  tfr1onlembfn  6488  tfrcllembacc  6499  tfrcllembfn  6501  frecabcl  6543  nnaordex  6672  nnawordex  6673  ectocld  6746  phpm  7023  dif1enen  7038  fin0  7043  fin0or  7044  fimax2gtri  7059  fidcenum  7119  suplub2ti  7164  supisoex  7172  enomnilem  7301  finomni  7303  enmkvlem  7324  exmidfodomrlemeldju  7373  exmidfodomrlemreseldju  7374  ltexnqq  7591  ltbtwnnqq  7598  prarloclem4  7681  prarloc2  7687  genprndl  7704  genprndu  7705  prmuloc2  7750  1idprl  7773  1idpru  7774  cauappcvgprlemdisj  7834  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  recexgt0sr  7956  map2psrprg  7988  suplocsrlem  7991  nntopi  8077  cnegexlem1  8317  cnegexlem2  8318  renegcl  8403  aptap  8793  supinfneg  9786  infsupneg  9787  qmulz  9814  elpq  9840  icc0r  10118  exbtwnzlemstep  10462  rebtwn2zlemstep  10467  ioo0  10474  ico0  10476  ioc0  10477  modqmuladd  10583  addmodlteq  10615  frec2uzrand  10622  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  hashunlem  11021  reuccatpfxs1lem  11273  shftlem  11322  caucvgre  11487  resqrexlemgt0  11526  rexico  11727  negfi  11734  climuni  11799  climshftlemg  11808  climcn1  11814  serf0  11858  summodclem2  11888  zsumdc  11890  fsum2dlemstep  11940  mertenslem2  12042  ntrivcvgap  12054  zproddc  12085  fprod2dlemstep  12128  dvds1lem  12308  odd2np1lem  12378  odd2np1  12379  sqoddm1div8z  12392  ltoddhalfle  12399  halfleoddlt  12400  m1expo  12406  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  flodddiv4  12442  bezoutlemaz  12519  bezoutlembz  12520  dvdssqim  12540  ncoprmgcdne1b  12606  coprmdvds2  12610  divgcdcoprm0  12618  cncongr1  12620  cncongr2  12621  dvdsnprmd  12642  rpexp  12670  pythagtriplem1  12783  pc2dvds  12848  difsqpwdvds  12856  oddprmdvds  12872  prmpwdvds  12873  4sqlem11  12919  imasmnd2  13480  dfgrp3mlem  13626  imasgrp2  13642  issubg4m  13725  imasabl  13868  ringinvnzdiv  14008  imasring  14022  dvdsrcl2  14057  dvdsrmul1  14060  isnzr2  14142  lss1d  14341  lssats2  14372  lspsn  14374  dvdsrzring  14561  znunit  14617  znrrg  14618  tgcl  14732  innei  14831  cnptoprest  14907  lmss  14914  lmtopcnp  14918  txlm  14947  blssps  15095  blss  15096  blssexps  15097  blssex  15098  mopni3  15152  metrest  15174  metcnp3  15179  mulc1cncf  15257  cncfco  15259  elply2  15403  gausslemma2dlem1a  15731  lgsquadlem1  15750  2lgsoddprmlem2  15779  subctctexmid  16325