Theorem rexlimdva 2623

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  rexlimdvaa  2624  rexlimivv  2629  rexlimdvv  2630  ralxfrd  4509  rexxfrd  4510  fvelimab  5635  foco2  5822  elunirn  5835  f1elima  5842  mpoexw  6299  tfrlem5  6400  tfrlemibacc  6412  tfrlemibfn  6414  tfr1onlembacc  6428  tfr1onlembfn  6430  tfrcllembacc  6441  tfrcllembfn  6443  frecabcl  6485  nnaordex  6614  nnawordex  6615  ectocld  6688  phpm  6962  dif1enen  6977  fin0  6982  fin0or  6983  fimax2gtri  6998  fidcenum  7058  suplub2ti  7103  supisoex  7111  enomnilem  7240  finomni  7242  enmkvlem  7263  exmidfodomrlemeldju  7307  exmidfodomrlemreseldju  7308  ltexnqq  7521  ltbtwnnqq  7528  prarloclem4  7611  prarloc2  7617  genprndl  7634  genprndu  7635  prmuloc2  7680  1idprl  7703  1idpru  7704  cauappcvgprlemdisj  7764  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemladdrl  7791  recexgt0sr  7886  map2psrprg  7918  suplocsrlem  7921  nntopi  8007  cnegexlem1  8247  cnegexlem2  8248  renegcl  8333  aptap  8723  supinfneg  9716  infsupneg  9717  qmulz  9744  elpq  9770  icc0r  10048  exbtwnzlemstep  10390  rebtwn2zlemstep  10395  ioo0  10402  ico0  10404  ioc0  10405  modqmuladd  10511  addmodlteq  10543  frec2uzrand  10550  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  hashunlem  10949  shftlem  11127  caucvgre  11292  resqrexlemgt0  11331  rexico  11532  negfi  11539  climuni  11604  climshftlemg  11613  climcn1  11619  serf0  11663  summodclem2  11693  zsumdc  11695  fsum2dlemstep  11745  mertenslem2  11847  ntrivcvgap  11859  zproddc  11890  fprod2dlemstep  11933  dvds1lem  12113  odd2np1lem  12183  odd2np1  12184  sqoddm1div8z  12197  ltoddhalfle  12204  halfleoddlt  12205  m1expo  12211  divalglemeunn  12232  divalglemex  12233  divalglemeuneg  12234  flodddiv4  12247  bezoutlemaz  12324  bezoutlembz  12325  dvdssqim  12345  ncoprmgcdne1b  12411  coprmdvds2  12415  divgcdcoprm0  12423  cncongr1  12425  cncongr2  12426  dvdsnprmd  12447  rpexp  12475  pythagtriplem1  12588  pc2dvds  12653  difsqpwdvds  12661  oddprmdvds  12677  prmpwdvds  12678  4sqlem11  12724  imasmnd2  13284  dfgrp3mlem  13430  imasgrp2  13446  issubg4m  13529  imasabl  13672  ringinvnzdiv  13812  imasring  13826  dvdsrcl2  13861  dvdsrmul1  13864  isnzr2  13946  lss1d  14145  lssats2  14176  lspsn  14178  dvdsrzring  14365  znunit  14421  znrrg  14422  tgcl  14536  innei  14635  cnptoprest  14711  lmss  14718  lmtopcnp  14722  txlm  14751  blssps  14899  blss  14900  blssexps  14901  blssex  14902  mopni3  14956  metrest  14978  metcnp3  14983  mulc1cncf  15061  cncfco  15063  elply2  15207  gausslemma2dlem1a  15535  lgsquadlem1  15554  2lgsoddprmlem2  15583  subctctexmid  15937