Theorem rexlimdva 2668

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  rexlimdvaa  2669  rexlimivv  2674  rexlimdvv  2675  ralxfrd  4603  rexxfrd  4604  fvelimab  5753  foco2  5949  elunirn  5962  f1elima  5969  mpoexw  6439  tfrlem5  6575  tfrlemibacc  6587  tfrlemibfn  6589  tfr1onlembacc  6603  tfr1onlembfn  6605  tfrcllembacc  6616  tfrcllembfn  6618  frecabcl  6660  nnaordex  6791  nnawordex  6792  ectocld  6865  phpm  7157  dif1enen  7174  fin0  7179  fin0or  7180  fimax2gtri  7196  fidcenum  7263  suplub2ti  7331  supisoex  7339  enomnilem  7468  finomni  7470  enmkvlem  7491  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  ltexnqq  7765  ltbtwnnqq  7772  prarloclem4  7855  prarloc2  7861  genprndl  7878  genprndu  7879  prmuloc2  7924  1idprl  7947  1idpru  7948  cauappcvgprlemdisj  8008  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  recexgt0sr  8130  map2psrprg  8162  suplocsrlem  8165  nntopi  8251  cnegexlem1  8491  cnegexlem2  8492  renegcl  8577  aptap  8968  supinfneg  9974  infsupneg  9975  qmulz  10002  elpq  10028  icc0r  10307  exbtwnzlemstep  10660  rebtwn2zlemstep  10665  ioo0  10672  ico0  10674  ioc0  10675  modqmuladd  10781  addmodlteq  10813  frec2uzrand  10820  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  hashunlem  11222  reuccatpfxs1lem  11496  shftlem  11559  caucvgre  11725  resqrexlemgt0  11764  rexico  11965  negfi  11972  climuni  12037  climshftlemg  12046  climcn1  12052  serf0  12096  summodclem2  12127  zsumdc  12129  fsum2dlemstep  12179  mertenslem2  12281  ntrivcvgap  12293  zproddc  12324  fprod2dlemstep  12367  dvds1lem  12547  odd2np1lem  12617  odd2np1  12618  sqoddm1div8z  12631  ltoddhalfle  12638  halfleoddlt  12639  m1expo  12645  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  flodddiv4  12681  bezoutlemaz  12758  bezoutlembz  12759  dvdssqim  12779  ncoprmgcdne1b  12845  coprmdvds2  12849  divgcdcoprm0  12857  cncongr1  12859  cncongr2  12860  dvdsnprmd  12881  rpexp  12909  pythagtriplem1  13022  pc2dvds  13087  difsqpwdvds  13095  oddprmdvds  13111  prmpwdvds  13112  4sqlem11  13158  imasmnd2  13736  dfgrp3mlem  13880  imasgrp2  13890  issubg4m  13973  imasabl  14117  ringinvnzdiv  14328  imasring  14342  dvdsrcl2  14379  dvdsrmul1  14382  isnzr2  14464  lss1d  14692  lssats2  14723  lspsn  14725  dvdsrzring  14910  znunit  14966  znrrg  14967  tgcl  15088  innei  15187  cnptoprest  15263  lmss  15270  lmtopcnp  15274  txlm  15303  blssps  15451  blss  15452  blssexps  15453  blssex  15454  mopni3  15508  metrest  15530  metcnp3  15535  mulc1cncf  15613  cncfco  15615  elply2  15759  gausslemma2dlem1a  16091  lgsquadlem1  16110  2lgsoddprmlem2  16139  uhgrspansubgrlem  16431  pw1ndom3  16934  subctctexmid  16944