Theorem ralrimdv 2968

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.)

Hypothesis

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

Assertion

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

Distinct variable groups:   ph, x   ps, x

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

Proof of Theorem ralrimdv

Step	Hyp	Ref	Expression
1		ralrimdv.1	. . . 4 |- ( ph -> ( ps -> ( x e. A -> ch ) ) )
2	1	imp 445	. . 3 |- ( ( ph /\ ps ) -> ( x e. A -> ch ) )
3	2	ralrimiv 2965	. 2 |- ( ( ph /\ ps ) -> A. x e. A ch )
4	3	ex 450	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:  ralrimdva  2969  ralrimivv  2970  wefrc  5108  oneqmin  7005  nneneq  8143  cflm  9072  coflim  9083  isf32lem12  9186  axdc3lem2  9273  zorn2lem7  9324  axpre-sup  9990  zmax  11785  zbtwnre  11786  supxrunb2  12150  fzrevral  12425  islss4  18962  topbas  20776  elcls3  20887  neips  20917  clslp  20952  subbascn  21058  cnpnei  21068  comppfsc  21335  fgss2  21678  fbflim2  21781  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  metcnp3  22345  aalioulem3  24089  brbtwn2  25785  hial0  27959  hial02  27960  ococss  28152  lnopmi  28859  adjlnop  28945  pjss2coi  29023  pj3cor1i  29068  strlem3a  29111  hstrlem3a  29119  mdbr3  29156  mdbr4  29157  dmdmd  29159  dmdbr3  29164  dmdbr4  29165  dmdbr5  29167  ssmd2  29171  mdslmd1i  29188  mdsymlem7  29268  cdj1i  29292  cdj3lem2b  29296  lub0N  34476  glb0N  34480  hlrelat2  34689  snatpsubN  35036  pmaple  35047  pclclN  35177  pclfinN  35186  pclfinclN  35236  ltrneq2  35434  trlval2  35450  trlord  35857  trintALT  39117  lindslinindsimp2  42252