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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   E.wrex 2529

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  rexlimdvaa  2669  rexlimivv  2674  rexlimdvv  2675  ralxfrd  4608  rexxfrd  4609  fvelimab  5759  foco2  5959  elunirn  5972  f1elima  5979  mpoexw  6449  tfrlem5  6585  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  frecabcl  6670  nnaordex  6801  nnawordex  6802  ectocld  6875  phpm  7167  dif1enen  7184  fin0  7189  fin0or  7190  fimax2gtri  7206  fidcenum  7273  suplub2ti  7342  supisoex  7350  enomnilem  7479  finomni  7481  enmkvlem  7502  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  ltexnqq  7776  ltbtwnnqq  7783  prarloclem4  7866  prarloc2  7872  genprndl  7889  genprndu  7890  prmuloc2  7935  1idprl  7958  1idpru  7959  cauappcvgprlemdisj  8019  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  recexgt0sr  8141  map2psrprg  8173  suplocsrlem  8176  nntopi  8262  cnegexlem1  8503  cnegexlem2  8504  renegcl  8589  aptap  8981  supinfneg  10005  infsupneg  10006  qmulz  10033  elpq  10060  icc0r  10339  exbtwnzlemstep  10693  rebtwn2zlemstep  10698  ioo0  10705  ico0  10707  ioc0  10708  modqmuladd  10818  addmodlteq  10850  frec2uzrand  10857  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  hashunlem  11260  reuccatpfxs1lem  11534  shftlem  11597  caucvgre  11763  resqrexlemgt0  11802  rexico  12004  negfi  12011  climuni  12078  climshftlemg  12087  climcn1  12093  serf0  12137  summodclem2  12168  zsumdc  12170  fsum2dlemstep  12220  mertenslem2  12322  ntrivcvgap  12334  zproddc  12365  fprod2dlemstep  12408  dvds1lem  12588  odd2np1lem  12658  odd2np1  12659  sqoddm1div8z  12672  ltoddhalfle  12679  halfleoddlt  12680  m1expo  12686  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  flodddiv4  12722  bezoutlemaz  12799  bezoutlembz  12800  dvdssqim  12820  ncoprmgcdne1b  12886  coprmdvds2  12890  divgcdcoprm0  12898  cncongr1  12900  cncongr2  12901  dvdsnprmd  12922  rpexp  12951  pythagtriplem1  13067  pc2dvds  13132  difsqpwdvds  13140  oddprmdvds  13156  prmpwdvds  13157  4sqlem11  13203  imasmnd2  13812  dfgrp3mlem  13956  imasgrp2  13966  issubg4m  14049  imasabl  14224  ringinvnzdiv  14439  imasring  14453  dvdsrcl2  14490  dvdsrmul1  14493  isnzr2  14575  lss1d  14804  lssats2  14835  lspsn  14837  dvdsrzring  15022  znunit  15078  znrrg  15079  tgcl  15256  innei  15355  cnptoprest  15431  lmss  15438  lmtopcnp  15442  txlm  15471  blssps  15619  blss  15620  blssexps  15621  blssex  15622  mopni3  15676  metrest  15698  metcnp3  15703  mulc1cncf  15781  cncfco  15783  elply2  15927  gausslemma2dlem1a  16343  lgsquadlem1  16362  2lgsoddprmlem2  16391  uhgrspansubgrlem  16683  pw1ndom3  17186  subctctexmid  17196