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  6589  tfrlemibacc  6601  tfrlemibfn  6603  tfr1onlembacc  6617  tfr1onlembfn  6619  tfrcllembacc  6630  tfrcllembfn  6632  frecabcl  6674  nnaordex  6805  nnawordex  6806  ectocld  6879  phpm  7171  dif1enen  7188  fin0  7193  fin0or  7194  fimax2gtri  7210  fidcenum  7278  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  10011  infsupneg  10012  qmulz  10039  elpq  10066  icc0r  10345  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  ioo0  10711  ico0  10713  ioc0  10714  modqmuladd  10824  addmodlteq  10856  frec2uzrand  10863  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  hashunlem  11266  reuccatpfxs1lem  11540  shftlem  11603  caucvgre  11769  resqrexlemgt0  11808  rexico  12010  negfi  12017  climuni  12084  climshftlemg  12093  climcn1  12099  serf0  12143  summodclem2  12174  zsumdc  12176  fsum2dlemstep  12226  mertenslem2  12328  ntrivcvgap  12340  zproddc  12371  fprod2dlemstep  12414  dvds1lem  12594  odd2np1lem  12664  odd2np1  12665  sqoddm1div8z  12678  ltoddhalfle  12685  halfleoddlt  12686  m1expo  12692  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  flodddiv4  12728  bezoutlemaz  12805  bezoutlembz  12806  dvdssqim  12826  ncoprmgcdne1b  12892  coprmdvds2  12896  divgcdcoprm0  12904  cncongr1  12906  cncongr2  12907  dvdsnprmd  12928  rpexp  12957  pythagtriplem1  13073  pc2dvds  13138  difsqpwdvds  13146  oddprmdvds  13162  prmpwdvds  13163  4sqlem11  13209  imasmnd2  13818  dfgrp3mlem  13962  imasgrp2  13972  issubg4m  14055  imasabl  14230  ringinvnzdiv  14462  imasring  14478  dvdsrcl2  14515  dvdsrmul1  14518  isnzr2  14600  lss1d  14829  lssats2  14860  lspsn  14862  dvdsrzring  15047  znunit  15103  znrrg  15104  tgcl  15290  innei  15389  cnptoprest  15465  lmss  15472  lmtopcnp  15476  txlm  15505  blssps  15653  blss  15654  blssexps  15655  blssex  15656  mopni3  15710  metrest  15732  metcnp3  15737  mulc1cncf  15815  cncfco  15817  elply2  15961  efnthr  16176  gausslemma2dlem1a  16382  lgsquadlem1  16401  2lgsoddprmlem2  16430  uhgrspansubgrlem  16722  pw1ndom3  17225  subctctexmid  17235