Theorem rexlimdva 2660

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  rexlimdvaa  2661  rexlimivv  2666  rexlimdvv  2667  ralxfrd  4583  rexxfrd  4584  fvelimab  5733  foco2  5926  elunirn  5939  f1elima  5946  mpoexw  6409  tfrlem5  6545  tfrlemibacc  6557  tfrlemibfn  6559  tfr1onlembacc  6573  tfr1onlembfn  6575  tfrcllembacc  6586  tfrcllembfn  6588  frecabcl  6630  nnaordex  6761  nnawordex  6762  ectocld  6835  phpm  7120  dif1enen  7137  fin0  7142  fin0or  7143  fimax2gtri  7159  fidcenum  7226  suplub2ti  7292  supisoex  7300  enomnilem  7429  finomni  7431  enmkvlem  7452  exmidfodomrlemeldju  7502  exmidfodomrlemreseldju  7503  ltexnqq  7723  ltbtwnnqq  7730  prarloclem4  7813  prarloc2  7819  genprndl  7836  genprndu  7837  prmuloc2  7882  1idprl  7905  1idpru  7906  cauappcvgprlemdisj  7966  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  recexgt0sr  8088  map2psrprg  8120  suplocsrlem  8123  nntopi  8209  cnegexlem1  8448  cnegexlem2  8449  renegcl  8534  aptap  8924  supinfneg  9927  infsupneg  9928  qmulz  9955  elpq  9981  icc0r  10259  exbtwnzlemstep  10607  rebtwn2zlemstep  10612  ioo0  10619  ico0  10621  ioc0  10622  modqmuladd  10728  addmodlteq  10760  frec2uzrand  10767  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  hashunlem  11168  reuccatpfxs1lem  11438  shftlem  11501  caucvgre  11666  resqrexlemgt0  11705  rexico  11906  negfi  11913  climuni  11978  climshftlemg  11987  climcn1  11993  serf0  12037  summodclem2  12068  zsumdc  12070  fsum2dlemstep  12120  mertenslem2  12222  ntrivcvgap  12234  zproddc  12265  fprod2dlemstep  12308  dvds1lem  12488  odd2np1lem  12558  odd2np1  12559  sqoddm1div8z  12572  ltoddhalfle  12579  halfleoddlt  12580  m1expo  12586  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  flodddiv4  12622  bezoutlemaz  12699  bezoutlembz  12700  dvdssqim  12720  ncoprmgcdne1b  12786  coprmdvds2  12790  divgcdcoprm0  12798  cncongr1  12800  cncongr2  12801  dvdsnprmd  12822  rpexp  12850  pythagtriplem1  12963  pc2dvds  13028  difsqpwdvds  13036  oddprmdvds  13052  prmpwdvds  13053  4sqlem11  13099  imasmnd2  13665  dfgrp3mlem  13811  imasgrp2  13827  issubg4m  13910  imasabl  14053  ringinvnzdiv  14194  imasring  14208  dvdsrcl2  14244  dvdsrmul1  14247  isnzr2  14329  lss1d  14531  lssats2  14562  lspsn  14564  dvdsrzring  14751  znunit  14807  znrrg  14808  tgcl  14929  innei  15028  cnptoprest  15104  lmss  15111  lmtopcnp  15115  txlm  15144  blssps  15292  blss  15293  blssexps  15294  blssex  15295  mopni3  15349  metrest  15371  metcnp3  15376  mulc1cncf  15454  cncfco  15456  elply2  15600  gausslemma2dlem1a  15931  lgsquadlem1  15950  2lgsoddprmlem2  15979  uhgrspansubgrlem  16271  pw1ndom3  16764  subctctexmid  16774