Theorem rexlimdva 2614

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  rexlimdvaa  2615  rexlimivv  2620  rexlimdvv  2621  ralxfrd  4498  rexxfrd  4499  fvelimab  5620  foco2  5803  elunirn  5816  f1elima  5823  mpoexw  6280  tfrlem5  6381  tfrlemibacc  6393  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembfn  6424  frecabcl  6466  nnaordex  6595  nnawordex  6596  ectocld  6669  phpm  6935  dif1enen  6950  fin0  6955  fin0or  6956  fimax2gtri  6971  fidcenum  7031  suplub2ti  7076  supisoex  7084  enomnilem  7213  finomni  7215  enmkvlem  7236  exmidfodomrlemeldju  7280  exmidfodomrlemreseldju  7281  ltexnqq  7494  ltbtwnnqq  7501  prarloclem4  7584  prarloc2  7590  genprndl  7607  genprndu  7608  prmuloc2  7653  1idprl  7676  1idpru  7677  cauappcvgprlemdisj  7737  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemladdrl  7764  recexgt0sr  7859  map2psrprg  7891  suplocsrlem  7894  nntopi  7980  cnegexlem1  8220  cnegexlem2  8221  renegcl  8306  aptap  8696  supinfneg  9688  infsupneg  9689  qmulz  9716  elpq  9742  icc0r  10020  exbtwnzlemstep  10356  rebtwn2zlemstep  10361  ioo0  10368  ico0  10370  ioc0  10371  modqmuladd  10477  addmodlteq  10509  frec2uzrand  10516  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  hashunlem  10915  shftlem  11000  caucvgre  11165  resqrexlemgt0  11204  rexico  11405  negfi  11412  climuni  11477  climshftlemg  11486  climcn1  11492  serf0  11536  summodclem2  11566  zsumdc  11568  fsum2dlemstep  11618  mertenslem2  11720  ntrivcvgap  11732  zproddc  11763  fprod2dlemstep  11806  dvds1lem  11986  odd2np1lem  12056  odd2np1  12057  sqoddm1div8z  12070  ltoddhalfle  12077  halfleoddlt  12078  m1expo  12084  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  flodddiv4  12120  bezoutlemaz  12197  bezoutlembz  12198  dvdssqim  12218  ncoprmgcdne1b  12284  coprmdvds2  12288  divgcdcoprm0  12296  cncongr1  12298  cncongr2  12299  dvdsnprmd  12320  rpexp  12348  pythagtriplem1  12461  pc2dvds  12526  difsqpwdvds  12534  oddprmdvds  12550  prmpwdvds  12551  4sqlem11  12597  imasmnd2  13156  dfgrp3mlem  13302  imasgrp2  13318  issubg4m  13401  imasabl  13544  ringinvnzdiv  13684  imasring  13698  dvdsrcl2  13733  dvdsrmul1  13736  isnzr2  13818  lss1d  14017  lssats2  14048  lspsn  14050  dvdsrzring  14237  znunit  14293  znrrg  14294  tgcl  14408  innei  14507  cnptoprest  14583  lmss  14590  lmtopcnp  14594  txlm  14623  blssps  14771  blss  14772  blssexps  14773  blssex  14774  mopni3  14828  metrest  14850  metcnp3  14855  mulc1cncf  14933  cncfco  14935  elply2  15079  gausslemma2dlem1a  15407  lgsquadlem1  15426  2lgsoddprmlem2  15455  subctctexmid  15755