Theorem rexlimdvaa 3032

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypothesis

Ref	Expression
rexlimdvaa.1	|- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )

Assertion

Ref	Expression
rexlimdvaa	|- ( ph -> ( E. x e. A ps -> ch ) )

Distinct variable groups:   ph, x   ch, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimdvaa

Step	Hyp	Ref	Expression
1		rexlimdvaa.1	. . 3 |- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )
2	1	expr 643	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	rexlimdva 3031	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexlimddv  3035  tz7.7  5749  isofrlem  6590  nnawordex  7717  oaabs2  7725  fiin  8328  marypha1lem  8339  wemaplem3  8453  cantnflt  8569  fseqenlem2  8848  cardaleph  8912  coftr  9095  fin23lem26  9147  fin1a2lem13  9234  fpwwe2  9465  r1wunlim  9559  wunex2  9560  inttsk  9596  grur1  9642  inaprc  9658  receu  10672  zsupss  11777  xralrple  12036  rexanuz  14085  limsupval2  14211  caucvgb  14410  fsumiun  14553  rpnnen2lem12  14954  dvdsval2  14986  prmind2  15398  pcprmpw2  15586  pockthg  15610  prmreclem5  15624  vdwlem6  15690  vdwlem10  15694  sscpwex  16475  drsdirfi  16938  psgnunilem3  17916  sylow3lem2  18043  efgsfo  18152  lt6abl  18296  ghmcyg  18297  unitgrp  18667  irredrmul  18707  drngnidl  19229  znunit  19912  tgcl  20773  neiint  20908  restopnb  20979  ordtrest2lem  21007  pnfnei  21024  mnfnei  21025  iscnp4  21067  haust1  21156  ordthauslem  21187  tgcmp  21204  t1connperf  21239  2ndc1stc  21254  2ndcdisj  21259  islly2  21287  nllyrest  21289  reftr  21317  comppfsc  21335  ptbasfi  21384  ptcnp  21425  xkococnlem  21462  tgqtop  21515  fbssfi  21641  fgabs  21683  neifil  21684  trfil2  21691  elfm2  21752  elfm3  21754  rnelfmlem  21756  fmfnfmlem4  21761  flffbas  21799  fclsfnflim  21831  ptcmplem4  21859  tsmsxp  21958  blssexps  22231  blssex  22232  icccmplem3  22627  cnheibor  22754  pi1blem  22839  iscfil3  23071  iscmet3lem2  23090  cmetss  23113  ovolicc2  23290  nulmbl2  23304  volsup  23324  dyadmbllem  23367  itg2const2  23508  bddmulibl  23605  limcflf  23645  itgsubst  23812  ulmdvlem3  24156  xrlimcnp  24695  amgm  24717  dchrptlem2  24990  lgsne0  25060  lgsqr  25076  lgsquadlem1  25105  dchrvmasumif  25192  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem3  25208  dchrisum0  25209  dchrmusum  25213  dchrvmasum  25214  chpdifbnd  25244  pntrlog2bnd  25273  pntibndlem3  25281  pntibnd  25282  pntleml  25300  ostth  25328  brbtwn2  25785  colinearalg  25790  nbumgrvtx  26242  cusgrfilem1  26351  nmobndi  27630  spansneleq  28429  ofrn2  29442  xreceu  29630  ordtrest2NEWlem  29968  dya2iocnei  30344  connpconn  31217  cvmsss2  31256  cvmlift2lem10  31294  cvmlift3lem2  31302  nosupno  31849  nosupbnd1lem1  31854  nosupbnd2  31862  scutbdaybnd  31921  outsidele  32239  neibastop1  32354  neibastop2lem  32355  matunitlindflem1  33405  mblfinlem1  33446  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  cnambfre  33458  itg2addnclem  33461  itg2addnclem3  33463  bddiblnc  33480  ftc1anclem7  33491  ftc1anc  33493  fdc  33541  sstotbnd2  33573  sstotbnd  33574  isbndx  33581  ssbnd  33587  totbndbnd  33588  heibor  33620  unichnidl  33830  pexmidlem8N  35263  elrfi  37257  fnwe2lem2  37621  hbtlem5  37698  liminfval2  40000  2zrngamgm  41939