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  4497  rexxfrd  4498  fvelimab  5617  foco2  5800  elunirn  5813  f1elima  5820  mpoexw  6271  tfrlem5  6372  tfrlemibacc  6384  tfrlemibfn  6386  tfr1onlembacc  6400  tfr1onlembfn  6402  tfrcllembacc  6413  tfrcllembfn  6415  frecabcl  6457  nnaordex  6586  nnawordex  6587  ectocld  6660  phpm  6926  dif1enen  6941  fin0  6946  fin0or  6947  fimax2gtri  6962  fidcenum  7022  suplub2ti  7067  supisoex  7075  enomnilem  7204  finomni  7206  enmkvlem  7227  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  ltexnqq  7475  ltbtwnnqq  7482  prarloclem4  7565  prarloc2  7571  genprndl  7588  genprndu  7589  prmuloc2  7634  1idprl  7657  1idpru  7658  cauappcvgprlemdisj  7718  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  recexgt0sr  7840  map2psrprg  7872  suplocsrlem  7875  nntopi  7961  cnegexlem1  8201  cnegexlem2  8202  renegcl  8287  aptap  8677  supinfneg  9669  infsupneg  9670  qmulz  9697  elpq  9723  icc0r  10001  exbtwnzlemstep  10337  rebtwn2zlemstep  10342  ioo0  10349  ico0  10351  ioc0  10352  modqmuladd  10458  addmodlteq  10490  frec2uzrand  10497  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  hashunlem  10896  shftlem  10981  caucvgre  11146  resqrexlemgt0  11185  rexico  11386  negfi  11393  climuni  11458  climshftlemg  11467  climcn1  11473  serf0  11517  summodclem2  11547  zsumdc  11549  fsum2dlemstep  11599  mertenslem2  11701  ntrivcvgap  11713  zproddc  11744  fprod2dlemstep  11787  dvds1lem  11967  odd2np1lem  12037  odd2np1  12038  sqoddm1div8z  12051  ltoddhalfle  12058  halfleoddlt  12059  m1expo  12065  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  flodddiv4  12101  bezoutlemaz  12170  bezoutlembz  12171  dvdssqim  12191  ncoprmgcdne1b  12257  coprmdvds2  12261  divgcdcoprm0  12269  cncongr1  12271  cncongr2  12272  dvdsnprmd  12293  rpexp  12321  pythagtriplem1  12434  pc2dvds  12499  difsqpwdvds  12507  oddprmdvds  12523  prmpwdvds  12524  4sqlem11  12570  dfgrp3mlem  13230  imasgrp2  13240  issubg4m  13323  imasabl  13466  ringinvnzdiv  13606  imasring  13620  dvdsrcl2  13655  dvdsrmul1  13658  isnzr2  13740  lss1d  13939  lssats2  13970  lspsn  13972  dvdsrzring  14159  znunit  14215  znrrg  14216  tgcl  14300  innei  14399  cnptoprest  14475  lmss  14482  lmtopcnp  14486  txlm  14515  blssps  14663  blss  14664  blssexps  14665  blssex  14666  mopni3  14720  metrest  14742  metcnp3  14747  mulc1cncf  14825  cncfco  14827  elply2  14971  gausslemma2dlem1a  15299  lgsquadlem1  15318  2lgsoddprmlem2  15347  subctctexmid  15645