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

Theorem ralrimdv 2632
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 1605 . 2  |-  F/ x ph
2 nfv 1605 . 2  |-  F/ x ps
3 ralrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
41, 2, 3ralrimd 2631 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralrimdva  2633  ralrimivv  2634  wefrc  4387  oneqmin  4596  tfrlem1  6391  abianfp  6471  nneneq  7044  cflm  7876  coflim  7887  isf32lem12  7990  axdc3lem2  8077  zorn2lem7  8129  axpre-sup  8791  infmrcl  9733  zmax  10313  zbtwnre  10314  supxrunb2  10639  fzrevral  10866  islss4  15719  topbas  16710  elcls3  16820  neips  16850  clslp  16879  subbascn  16984  cnpnei  16993  fgss2  17569  fbflim2  17672  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  metcnp3  18086  aalioulem3  19714  hial0  21681  hial02  21682  ococss  21872  lnopmi  22580  adjlnop  22666  pjss2coi  22744  pj3cor1i  22789  strlem3a  22832  hstrlem3a  22840  mdbr3  22877  mdbr4  22878  dmdmd  22880  dmdbr3  22885  dmdbr4  22886  dmdbr5  22888  ssmd2  22892  mdslmd1i  22909  mdsymlem7  22989  cdj1i  23013  cdj3lem2b  23017  ghomf1olem  24001  brbtwn2  24533  comppfsc  26307  trintALT  28657  lub0N  29379  hlrelat2  29592  snatpsubN  29939  pmaple  29950  pclclN  30080  pclfinN  30089  pclfinclN  30139  ltrneq2  30337  trlval2  30352  trlord  30758
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator