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

Theorem ralrimdv 2603
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 2602 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   A.wral 2516
This theorem is referenced by:  ralrimdva  2604  ralrimivv  2605  wefrc  4324  oneqmin  4533  tfrlem1  6324  abianfp  6404  nneneq  6977  cflm  7809  coflim  7820  isf32lem12  7923  axdc3lem2  8010  zorn2lem7  8062  axpre-sup  8724  infmrcl  9666  zmax  10245  zbtwnre  10246  supxrunb2  10570  fzrevral  10797  islss4  15646  topbas  16637  elcls3  16747  neips  16777  clslp  16806  subbascn  16911  cnpnei  16920  fgss2  17496  fbflim2  17599  alexsubALTlem3  17670  alexsubALTlem4  17671  alexsubALT  17672  metcnp3  18013  aalioulem3  19641  hial0  21606  hial02  21607  ococss  21797  lnopmi  22505  adjlnop  22591  pjss2coi  22669  pj3cor1i  22714  strlem3a  22757  hstrlem3a  22765  mdbr3  22802  mdbr4  22803  dmdmd  22805  dmdbr3  22810  dmdbr4  22811  dmdbr5  22813  ssmd2  22817  mdslmd1i  22834  mdsymlem7  22914  cdj1i  22938  cdj3lem2b  22942  ghomf1olem  23338  brbtwn2  23873  comppfsc  25639  trintALT  27670  lub0N  28509  hlrelat2  28722  snatpsubN  29069  pmaple  29080  pclclN  29210  pclfinN  29219  pclfinclN  29269  ltrneq2  29467  trlval2  29482  trlord  29888
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540  df-ral 2520
  Copyright terms: Public domain W3C validator