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  4553  rexxfrd  4554  fvelimab  5692  foco2  5883  elunirn  5896  f1elima  5903  mpoexw  6365  tfrlem5  6466  tfrlemibacc  6478  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembfn  6509  frecabcl  6551  nnaordex  6682  nnawordex  6683  ectocld  6756  phpm  7035  dif1enen  7050  fin0  7055  fin0or  7056  fimax2gtri  7072  fidcenum  7134  suplub2ti  7179  supisoex  7187  enomnilem  7316  finomni  7318  enmkvlem  7339  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  ltexnqq  7606  ltbtwnnqq  7613  prarloclem4  7696  prarloc2  7702  genprndl  7719  genprndu  7720  prmuloc2  7765  1idprl  7788  1idpru  7789  cauappcvgprlemdisj  7849  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  recexgt0sr  7971  map2psrprg  8003  suplocsrlem  8006  nntopi  8092  cnegexlem1  8332  cnegexlem2  8333  renegcl  8418  aptap  8808  supinfneg  9802  infsupneg  9803  qmulz  9830  elpq  9856  icc0r  10134  exbtwnzlemstep  10479  rebtwn2zlemstep  10484  ioo0  10491  ico0  10493  ioc0  10494  modqmuladd  10600  addmodlteq  10632  frec2uzrand  10639  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  hashunlem  11038  reuccatpfxs1lem  11293  shftlem  11342  caucvgre  11507  resqrexlemgt0  11546  rexico  11747  negfi  11754  climuni  11819  climshftlemg  11828  climcn1  11834  serf0  11878  summodclem2  11908  zsumdc  11910  fsum2dlemstep  11960  mertenslem2  12062  ntrivcvgap  12074  zproddc  12105  fprod2dlemstep  12148  dvds1lem  12328  odd2np1lem  12398  odd2np1  12399  sqoddm1div8z  12412  ltoddhalfle  12419  halfleoddlt  12420  m1expo  12426  divalglemeunn  12447  divalglemex  12448  divalglemeuneg  12449  flodddiv4  12462  bezoutlemaz  12539  bezoutlembz  12540  dvdssqim  12560  ncoprmgcdne1b  12626  coprmdvds2  12630  divgcdcoprm0  12638  cncongr1  12640  cncongr2  12641  dvdsnprmd  12662  rpexp  12690  pythagtriplem1  12803  pc2dvds  12868  difsqpwdvds  12876  oddprmdvds  12892  prmpwdvds  12893  4sqlem11  12939  imasmnd2  13500  dfgrp3mlem  13646  imasgrp2  13662  issubg4m  13745  imasabl  13888  ringinvnzdiv  14028  imasring  14042  dvdsrcl2  14078  dvdsrmul1  14081  isnzr2  14163  lss1d  14362  lssats2  14393  lspsn  14395  dvdsrzring  14582  znunit  14638  znrrg  14639  tgcl  14753  innei  14852  cnptoprest  14928  lmss  14935  lmtopcnp  14939  txlm  14968  blssps  15116  blss  15117  blssexps  15118  blssex  15119  mopni3  15173  metrest  15195  metcnp3  15200  mulc1cncf  15278  cncfco  15280  elply2  15424  gausslemma2dlem1a  15752  lgsquadlem1  15771  2lgsoddprmlem2  15800  pw1ndom3  16413  subctctexmid  16425