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  7341  supisoex  7349  enomnilem  7478  finomni  7480  enmkvlem  7501  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  ltexnqq  7775  ltbtwnnqq  7782  prarloclem4  7865  prarloc2  7871  genprndl  7888  genprndu  7889  prmuloc2  7934  1idprl  7957  1idpru  7958  cauappcvgprlemdisj  8018  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  recexgt0sr  8140  map2psrprg  8172  suplocsrlem  8175  nntopi  8261  cnegexlem1  8501  cnegexlem2  8502  renegcl  8587  aptap  8978  supinfneg  9995  infsupneg  9996  qmulz  10023  elpq  10049  icc0r  10328  exbtwnzlemstep  10682  rebtwn2zlemstep  10687  ioo0  10694  ico0  10696  ioc0  10697  modqmuladd  10803  addmodlteq  10835  frec2uzrand  10842  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  hashunlem  11244  reuccatpfxs1lem  11518  shftlem  11581  caucvgre  11747  resqrexlemgt0  11786  rexico  11987  negfi  11994  climuni  12059  climshftlemg  12068  climcn1  12074  serf0  12118  summodclem2  12149  zsumdc  12151  fsum2dlemstep  12201  mertenslem2  12303  ntrivcvgap  12315  zproddc  12346  fprod2dlemstep  12389  dvds1lem  12569  odd2np1lem  12639  odd2np1  12640  sqoddm1div8z  12653  ltoddhalfle  12660  halfleoddlt  12661  m1expo  12667  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  flodddiv4  12703  bezoutlemaz  12780  bezoutlembz  12781  dvdssqim  12801  ncoprmgcdne1b  12867  coprmdvds2  12871  divgcdcoprm0  12879  cncongr1  12881  cncongr2  12882  dvdsnprmd  12903  rpexp  12931  pythagtriplem1  13044  pc2dvds  13109  difsqpwdvds  13117  oddprmdvds  13133  prmpwdvds  13134  4sqlem11  13180  imasmnd2  13759  dfgrp3mlem  13903  imasgrp2  13913  issubg4m  13996  imasabl  14140  ringinvnzdiv  14355  imasring  14369  dvdsrcl2  14406  dvdsrmul1  14409  isnzr2  14491  lss1d  14720  lssats2  14751  lspsn  14753  dvdsrzring  14938  znunit  14994  znrrg  14995  tgcl  15165  innei  15264  cnptoprest  15340  lmss  15347  lmtopcnp  15351  txlm  15380  blssps  15528  blss  15529  blssexps  15530  blssex  15531  mopni3  15585  metrest  15607  metcnp3  15612  mulc1cncf  15690  cncfco  15692  elply2  15836  gausslemma2dlem1a  16177  lgsquadlem1  16196  2lgsoddprmlem2  16225  uhgrspansubgrlem  16517  pw1ndom3  17020  subctctexmid  17030