Theorem rexlimdva 2594

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  rexlimdvaa  2595  rexlimivv  2600  rexlimdvv  2601  ralxfrd  4464  rexxfrd  4465  fvelimab  5574  foco2  5756  elunirn  5769  f1elima  5776  mpoexw  6216  tfrlem5  6317  tfrlemibacc  6329  tfrlemibfn  6331  tfr1onlembacc  6345  tfr1onlembfn  6347  tfrcllembacc  6358  tfrcllembfn  6360  frecabcl  6402  nnaordex  6531  nnawordex  6532  ectocld  6603  phpm  6867  dif1enen  6882  fin0  6887  fin0or  6888  fimax2gtri  6903  fidcenum  6957  suplub2ti  7002  supisoex  7010  enomnilem  7138  finomni  7140  enmkvlem  7161  exmidfodomrlemeldju  7200  exmidfodomrlemreseldju  7201  ltexnqq  7409  ltbtwnnqq  7416  prarloclem4  7499  prarloc2  7505  genprndl  7522  genprndu  7523  prmuloc2  7568  1idprl  7591  1idpru  7592  cauappcvgprlemdisj  7652  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  caucvgprlemladdrl  7679  recexgt0sr  7774  map2psrprg  7806  suplocsrlem  7809  nntopi  7895  cnegexlem1  8134  cnegexlem2  8135  renegcl  8220  aptap  8609  supinfneg  9597  infsupneg  9598  qmulz  9625  elpq  9650  icc0r  9928  exbtwnzlemstep  10250  rebtwn2zlemstep  10255  ioo0  10262  ico0  10264  ioc0  10265  modqmuladd  10368  addmodlteq  10400  frec2uzrand  10407  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  hashunlem  10786  shftlem  10827  caucvgre  10992  resqrexlemgt0  11031  rexico  11232  negfi  11238  climuni  11303  climshftlemg  11312  climcn1  11318  serf0  11362  summodclem2  11392  zsumdc  11394  fsum2dlemstep  11444  mertenslem2  11546  ntrivcvgap  11558  zproddc  11589  fprod2dlemstep  11632  dvds1lem  11811  odd2np1lem  11879  odd2np1  11880  sqoddm1div8z  11893  ltoddhalfle  11900  halfleoddlt  11901  m1expo  11907  divalglemeunn  11928  divalglemex  11929  divalglemeuneg  11930  flodddiv4  11941  bezoutlemaz  12006  bezoutlembz  12007  dvdssqim  12027  ncoprmgcdne1b  12091  coprmdvds2  12095  divgcdcoprm0  12103  cncongr1  12105  cncongr2  12106  dvdsnprmd  12127  rpexp  12155  pythagtriplem1  12267  pc2dvds  12331  difsqpwdvds  12339  oddprmdvds  12354  prmpwdvds  12355  dfgrp3mlem  12973  issubg4m  13058  ringinvnzdiv  13232  dvdsrcl2  13273  dvdsrmul1  13276  lss1d  13475  lssats2  13505  lspsn  13507  dvdsrzring  13578  tgcl  13649  innei  13748  cnptoprest  13824  lmss  13831  lmtopcnp  13835  txlm  13864  blssps  14012  blss  14013  blssexps  14014  blssex  14015  mopni3  14069  metrest  14091  metcnp3  14096  mulc1cncf  14161  cncfco  14163  2lgsoddprmlem2  14539  subctctexmid  14835