Theorem rexlimdva 2549

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 114	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2548	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480   E.wrex 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421  df-rex 2422

This theorem is referenced by:  rexlimdvaa  2550  rexlimivv  2555  rexlimdvv  2556  ralxfrd  4383  rexxfrd  4384  fvelimab  5477  foco2  5655  elunirn  5667  f1elima  5674  tfrlem5  6211  tfrlemibacc  6223  tfrlemibfn  6225  tfr1onlembacc  6239  tfr1onlembfn  6241  tfrcllembacc  6252  tfrcllembfn  6254  frecabcl  6296  nnaordex  6423  nnawordex  6424  ectocld  6495  phpm  6759  dif1enen  6774  fin0  6779  fin0or  6780  fimax2gtri  6795  fidcenum  6844  suplub2ti  6888  supisoex  6896  enomnilem  7010  finomni  7012  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  ltexnqq  7216  ltbtwnnqq  7223  prarloclem4  7306  prarloc2  7312  genprndl  7329  genprndu  7330  prmuloc2  7375  1idprl  7398  1idpru  7399  cauappcvgprlemdisj  7459  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemladdrl  7486  recexgt0sr  7581  map2psrprg  7613  suplocsrlem  7616  nntopi  7702  cnegexlem1  7937  cnegexlem2  7938  renegcl  8023  supinfneg  9390  infsupneg  9391  qmulz  9415  icc0r  9709  exbtwnzlemstep  10025  rebtwn2zlemstep  10030  ioo0  10037  ico0  10039  ioc0  10040  modqmuladd  10139  addmodlteq  10171  frec2uzrand  10178  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  hashunlem  10550  shftlem  10588  caucvgre  10753  resqrexlemgt0  10792  rexico  10993  negfi  10999  climuni  11062  climshftlemg  11071  climcn1  11077  serf0  11121  summodclem2  11151  zsumdc  11153  fsum2dlemstep  11203  mertenslem2  11305  ntrivcvgap  11317  dvds1lem  11504  odd2np1lem  11569  odd2np1  11570  sqoddm1div8z  11583  ltoddhalfle  11590  halfleoddlt  11591  m1expo  11597  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  flodddiv4  11631  bezoutlemaz  11691  bezoutlembz  11692  dvdssqim  11712  ncoprmgcdne1b  11770  coprmdvds2  11774  divgcdcoprm0  11782  cncongr1  11784  cncongr2  11785  dvdsnprmd  11806  rpexp  11831  tgcl  12233  innei  12332  cnptoprest  12408  lmss  12415  lmtopcnp  12419  txlm  12448  blssps  12596  blss  12597  blssexps  12598  blssex  12599  mopni3  12653  metrest  12675  metcnp3  12680  mulc1cncf  12745  cncfco  12747  subctctexmid  13196