MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrimdv Unicode version

Theorem ralrimdv 2787
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.)
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
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2 nfv 1629 . 2  |-  F/ x ps
3 ralrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
41, 2, 3ralrimd 2786 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   A.wral 2697
This theorem is referenced by:  ralrimdva  2788  ralrimivv  2789  wefrc  4568  oneqmin  4776  tfrlem1  6627  abianfp  6707  nneneq  7281  cflm  8119  coflim  8130  isf32lem12  8233  axdc3lem2  8320  zorn2lem7  8371  axpre-sup  9033  infmrcl  9976  zmax  10560  zbtwnre  10561  supxrunb2  10888  fzrevral  11119  islss4  16026  topbas  17025  elcls3  17135  neips  17165  clslp  17200  subbascn  17306  cnpnei  17316  fgss2  17894  fbflim2  17997  alexsubALTlem3  18068  alexsubALTlem4  18069  alexsubALT  18070  metcnp3  18558  aalioulem3  20239  hial0  22592  hial02  22593  ococss  22783  lnopmi  23491  adjlnop  23577  pjss2coi  23655  pj3cor1i  23700  strlem3a  23743  hstrlem3a  23751  mdbr3  23788  mdbr4  23789  dmdmd  23791  dmdbr3  23796  dmdbr4  23797  dmdbr5  23799  ssmd2  23803  mdslmd1i  23820  mdsymlem7  23900  cdj1i  23924  cdj3lem2b  23928  ghomf1olem  25093  brbtwn2  25792  comppfsc  26324  trintALT  28847  lub0N  29826  hlrelat2  30039  snatpsubN  30386  pmaple  30397  pclclN  30527  pclfinN  30536  pclfinclN  30586  ltrneq2  30784  trlval2  30799  trlord  31205
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator