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  8502  cnegexlem2  8503  renegcl  8588  aptap  8980  supinfneg  10004  infsupneg  10005  qmulz  10032  elpq  10059  icc0r  10338  exbtwnzlemstep  10692  rebtwn2zlemstep  10697  ioo0  10704  ico0  10706  ioc0  10707  modqmuladd  10816  addmodlteq  10848  frec2uzrand  10855  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  hashunlem  11258  reuccatpfxs1lem  11532  shftlem  11595  caucvgre  11761  resqrexlemgt0  11800  rexico  12002  negfi  12009  climuni  12075  climshftlemg  12084  climcn1  12090  serf0  12134  summodclem2  12165  zsumdc  12167  fsum2dlemstep  12217  mertenslem2  12319  ntrivcvgap  12331  zproddc  12362  fprod2dlemstep  12405  dvds1lem  12585  odd2np1lem  12655  odd2np1  12656  sqoddm1div8z  12669  ltoddhalfle  12676  halfleoddlt  12677  m1expo  12683  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  flodddiv4  12719  bezoutlemaz  12796  bezoutlembz  12797  dvdssqim  12817  ncoprmgcdne1b  12883  coprmdvds2  12887  divgcdcoprm0  12895  cncongr1  12897  cncongr2  12898  dvdsnprmd  12919  rpexp  12948  pythagtriplem1  13064  pc2dvds  13129  difsqpwdvds  13137  oddprmdvds  13153  prmpwdvds  13154  4sqlem11  13200  imasmnd2  13808  dfgrp3mlem  13952  imasgrp2  13962  issubg4m  14045  imasabl  14189  ringinvnzdiv  14404  imasring  14418  dvdsrcl2  14455  dvdsrmul1  14458  isnzr2  14540  lss1d  14769  lssats2  14800  lspsn  14802  dvdsrzring  14987  znunit  15043  znrrg  15044  tgcl  15214  innei  15313  cnptoprest  15389  lmss  15396  lmtopcnp  15400  txlm  15429  blssps  15577  blss  15578  blssexps  15579  blssex  15580  mopni3  15634  metrest  15656  metcnp3  15661  mulc1cncf  15739  cncfco  15741  elply2  15885  gausslemma2dlem1a  16275  lgsquadlem1  16294  2lgsoddprmlem2  16323  uhgrspansubgrlem  16615  pw1ndom3  17118  subctctexmid  17128