Theorem rexlimdva 2650

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  rexlimdvaa  2651  rexlimivv  2656  rexlimdvv  2657  ralxfrd  4559  rexxfrd  4560  fvelimab  5702  foco2  5894  elunirn  5907  f1elima  5914  mpoexw  6378  tfrlem5  6480  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  frecabcl  6565  nnaordex  6696  nnawordex  6697  ectocld  6770  phpm  7052  dif1enen  7069  fin0  7074  fin0or  7075  fimax2gtri  7091  fidcenum  7155  suplub2ti  7200  supisoex  7208  enomnilem  7337  finomni  7339  enmkvlem  7360  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  ltexnqq  7628  ltbtwnnqq  7635  prarloclem4  7718  prarloc2  7724  genprndl  7741  genprndu  7742  prmuloc2  7787  1idprl  7810  1idpru  7811  cauappcvgprlemdisj  7871  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  recexgt0sr  7993  map2psrprg  8025  suplocsrlem  8028  nntopi  8114  cnegexlem1  8354  cnegexlem2  8355  renegcl  8440  aptap  8830  supinfneg  9829  infsupneg  9830  qmulz  9857  elpq  9883  icc0r  10161  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  ioo0  10520  ico0  10522  ioc0  10523  modqmuladd  10629  addmodlteq  10661  frec2uzrand  10668  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  hashunlem  11068  reuccatpfxs1lem  11328  shftlem  11378  caucvgre  11543  resqrexlemgt0  11582  rexico  11783  negfi  11790  climuni  11855  climshftlemg  11864  climcn1  11870  serf0  11914  summodclem2  11945  zsumdc  11947  fsum2dlemstep  11997  mertenslem2  12099  ntrivcvgap  12111  zproddc  12142  fprod2dlemstep  12185  dvds1lem  12365  odd2np1lem  12435  odd2np1  12436  sqoddm1div8z  12449  ltoddhalfle  12456  halfleoddlt  12457  m1expo  12463  divalglemeunn  12484  divalglemex  12485  divalglemeuneg  12486  flodddiv4  12499  bezoutlemaz  12576  bezoutlembz  12577  dvdssqim  12597  ncoprmgcdne1b  12663  coprmdvds2  12667  divgcdcoprm0  12675  cncongr1  12677  cncongr2  12678  dvdsnprmd  12699  rpexp  12727  pythagtriplem1  12840  pc2dvds  12905  difsqpwdvds  12913  oddprmdvds  12929  prmpwdvds  12930  4sqlem11  12976  imasmnd2  13537  dfgrp3mlem  13683  imasgrp2  13699  issubg4m  13782  imasabl  13925  ringinvnzdiv  14066  imasring  14080  dvdsrcl2  14116  dvdsrmul1  14119  isnzr2  14201  lss1d  14400  lssats2  14431  lspsn  14433  dvdsrzring  14620  znunit  14676  znrrg  14677  tgcl  14791  innei  14890  cnptoprest  14966  lmss  14973  lmtopcnp  14977  txlm  15006  blssps  15154  blss  15155  blssexps  15156  blssex  15157  mopni3  15211  metrest  15233  metcnp3  15238  mulc1cncf  15316  cncfco  15318  elply2  15462  gausslemma2dlem1a  15790  lgsquadlem1  15809  2lgsoddprmlem2  15838  uhgrspansubgrlem  16130  pw1ndom3  16610  subctctexmid  16622