Theorem ralrimdva 2969

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) (Proof shortened by Wolf Lammen, 28-Dec-2019.)

Hypothesis

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

Assertion

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

Distinct variable groups:   ph, x   ps, x

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

Proof of Theorem ralrimdva

Step	Hyp	Ref	Expression
1		ralrimdva.1	. . . 4 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	expimpd 629	. . 3 |- ( ph -> ( ( x e. A /\ ps ) -> ch ) )
3	2	expcomd 454	. 2 |- ( ph -> ( ps -> ( x e. A -> ch ) ) )
4	3	ralrimdv 2968	1 |- ( ph -> ( ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912

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-ral 2917

This theorem is referenced by:  ralxfrd  4879  ralxfrdOLD  4880  ralxfrd2  4884  isoselem  6591  resixpfo  7946  findcard  8199  ordtypelem2  8424  alephinit  8918  isfin2-2  9141  axpre-sup  9990  nnsub  11059  ublbneg  11773  xralrple  12036  supxrunb1  12149  expnlbnd2  12995  faclbnd4lem4  13083  hashbc  13237  cau3lem  14094  limsupbnd2  14214  climrlim2  14278  climshftlem  14305  subcn2  14325  isercoll  14398  climsup  14400  serf0  14411  iseralt  14415  incexclem  14568  sqrt2irr  14979  pclem  15543  prmpwdvds  15608  vdwlem10  15694  vdwlem13  15697  ramtlecl  15704  ramub  15717  ramcl  15733  iscatd  16334  clatleglb  17126  mrcmndind  17366  grpinveu  17456  dfgrp3lem  17513  issubg4  17613  gexdvds  17999  sylow2alem2  18033  obselocv  20072  scmatscm  20319  tgcn  21056  tgcnp  21057  lmconst  21065  cncls2  21077  cncls  21078  cnntr  21079  lmss  21102  cnt0  21150  isnrm2  21162  isreg2  21181  cmpsublem  21202  cmpsub  21203  tgcmp  21204  islly2  21287  kgencn2  21360  txdis  21435  txlm  21451  kqt0lem  21539  isr0  21540  regr1lem2  21543  cmphaushmeo  21603  cfinufil  21732  ufilen  21734  flimopn  21779  fbflim2  21781  fclsnei  21823  fclsbas  21825  fclsrest  21828  flimfnfcls  21832  fclscmp  21834  ufilcmp  21836  isfcf  21838  fcfnei  21839  cnpfcf  21845  tsmsres  21947  tsmsxp  21958  blbas  22235  prdsbl  22296  metss  22313  metcnp3  22345  bndth  22757  lebnumii  22765  iscfil3  23071  iscmet3lem1  23089  equivcfil  23097  equivcau  23098  ellimc3  23643  lhop1  23777  dvfsumrlim  23794  ftc1lem6  23804  fta1g  23927  dgrco  24031  plydivex  24052  fta1  24063  vieta1  24067  ulmshftlem  24143  ulmcaulem  24148  mtest  24158  cxpcn3lem  24488  cxploglim  24704  ftalem3  24801  dchrisumlem3  25180  pntibnd  25282  ostth2lem2  25323  grpoinveu  27373  nmcvcn  27550  blocnilem  27659  ubthlem3  27728  htthlem  27774  spansni  28416  bra11  28967  lmxrge0  29998  mrsubff1  31411  msubff1  31453  fnemeet2  32362  fnejoin2  32364  fin2so  33396  lindsenlbs  33404  poimirlem29  33438  poimirlem30  33439  ftc1cnnc  33484  incsequz2  33545  geomcau  33555  caushft  33557  sstotbnd2  33573  isbnd2  33582  totbndbnd  33588  ismtybndlem  33605  heibor  33620  atlatle  34607  cvlcvr1  34626  ltrnid  35421  ltrneq2  35434  climinf  39838  ralbinrald  41199  snlindsntorlem  42259