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  4610  rexxfrd  4611  fvelimab  5762  foco2  5962  elunirn  5975  f1elima  5982  mpoexw  6453  tfrlem5  6590  tfrlemibacc  6602  tfrlemibfn  6604  tfr1onlembacc  6618  tfr1onlembfn  6620  tfrcllembacc  6631  tfrcllembfn  6633  frecabcl  6675  nnaordex  6806  nnawordex  6807  ectocld  6880  phpm  7173  dif1enen  7190  fin0  7195  fin0or  7196  fimax2gtri  7212  fidcenum  7280  suplub2ti  7347  supisoex  7355  enomnilem  7484  finomni  7486  enmkvlem  7507  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  ltexnqq  7781  ltbtwnnqq  7788  prarloclem4  7871  prarloc2  7877  genprndl  7894  genprndu  7895  prmuloc2  7940  1idprl  7963  1idpru  7964  cauappcvgprlemdisj  8024  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  recexgt0sr  8146  map2psrprg  8178  suplocsrlem  8181  nntopi  8267  cnegexlem1  8508  cnegexlem2  8509  renegcl  8594  aptap  8986  supinfneg  10010  infsupneg  10011  qmulz  10038  elpq  10065  icc0r  10344  exbtwnzlemstep  10698  rebtwn2zlemstep  10703  ioo0  10710  ico0  10712  ioc0  10713  modqmuladd  10823  addmodlteq  10855  frec2uzrand  10862  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  hashunlem  11265  reuccatpfxs1lem  11539  shftlem  11602  caucvgre  11768  resqrexlemgt0  11807  rexico  12009  negfi  12016  climuni  12083  climshftlemg  12092  climcn1  12098  serf0  12142  summodclem2  12173  zsumdc  12175  fsum2dlemstep  12225  mertenslem2  12327  ntrivcvgap  12339  zproddc  12370  fprod2dlemstep  12413  dvds1lem  12593  odd2np1lem  12663  odd2np1  12664  sqoddm1div8z  12677  ltoddhalfle  12684  halfleoddlt  12685  m1expo  12691  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  flodddiv4  12727  bezoutlemaz  12804  bezoutlembz  12805  dvdssqim  12825  ncoprmgcdne1b  12891  coprmdvds2  12895  divgcdcoprm0  12903  cncongr1  12905  cncongr2  12906  dvdsnprmd  12927  rpexp  12956  pythagtriplem1  13072  pc2dvds  13137  difsqpwdvds  13145  oddprmdvds  13161  prmpwdvds  13162  4sqlem11  13208  imasmnd2  13817  dfgrp3mlem  13961  imasgrp2  13971  issubg4m  14054  imasabl  14229  ringinvnzdiv  14461  imasring  14477  dvdsrcl2  14514  dvdsrmul1  14517  isnzr2  14599  lss1d  14828  lssats2  14859  lspsn  14861  dvdsrzring  15046  znunit  15102  znrrg  15103  tgcl  15307  innei  15406  cnptoprest  15482  lmss  15489  lmtopcnp  15493  txlm  15522  blssps  15670  blss  15671  blssexps  15672  blssex  15673  mopni3  15727  metrest  15749  metcnp3  15754  mulc1cncf  15832  cncfco  15834  elply2  15978  efnthr  16193  gausslemma2dlem1a  16399  lgsquadlem1  16418  2lgsoddprmlem2  16447  uhgrspansubgrlem  16739  pw1ndom3  17242  subctctexmid  17252