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

Theorem ralrimdv 2605
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 2604 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  2606  ralrimivv  2607  wefrc  4345  oneqmin  4554  tfrlem1  6345  abianfp  6425  nneneq  6998  cflm  7830  coflim  7841  isf32lem12  7944  axdc3lem2  8031  zorn2lem7  8083  axpre-sup  8745  infmrcl  9687  zmax  10266  zbtwnre  10267  supxrunb2  10591  fzrevral  10818  islss4  15667  topbas  16658  elcls3  16768  neips  16798  clslp  16827  subbascn  16932  cnpnei  16941  fgss2  17517  fbflim2  17620  alexsubALTlem3  17691  alexsubALTlem4  17692  alexsubALT  17693  metcnp3  18034  aalioulem3  19662  hial0  21627  hial02  21628  ococss  21818  lnopmi  22526  adjlnop  22612  pjss2coi  22690  pj3cor1i  22735  strlem3a  22778  hstrlem3a  22786  mdbr3  22823  mdbr4  22824  dmdmd  22826  dmdbr3  22831  dmdbr4  22832  dmdbr5  22834  ssmd2  22838  mdslmd1i  22855  mdsymlem7  22935  cdj1i  22959  cdj3lem2b  22963  ghomf1olem  23359  brbtwn2  23894  comppfsc  25660  trintALT  27691  lub0N  28530  hlrelat2  28743  snatpsubN  29090  pmaple  29101  pclclN  29231  pclfinN  29240  pclfinclN  29290  ltrneq2  29488  trlval2  29503  trlord  29909
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 2521
  Copyright terms: Public domain W3C validator