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

Theorem ralrimdv 2633
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 1610 . 2  |-  F/ x ph
2 nfv 1610 . 2  |-  F/ x ps
3 ralrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
41, 2, 3ralrimd 2632 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1688   A.wral 2544
This theorem is referenced by:  ralrimdva  2634  ralrimivv  2635  wefrc  4386  oneqmin  4595  tfrlem1  6386  abianfp  6466  nneneq  7039  cflm  7871  coflim  7882  isf32lem12  7985  axdc3lem2  8072  zorn2lem7  8124  axpre-sup  8786  infmrcl  9728  zmax  10308  zbtwnre  10309  supxrunb2  10633  fzrevral  10860  islss4  15713  topbas  16704  elcls3  16814  neips  16844  clslp  16873  subbascn  16978  cnpnei  16987  fgss2  17563  fbflim2  17666  alexsubALTlem3  17737  alexsubALTlem4  17738  alexsubALT  17739  metcnp3  18080  aalioulem3  19708  hial0  21673  hial02  21674  ococss  21864  lnopmi  22572  adjlnop  22658  pjss2coi  22736  pj3cor1i  22781  strlem3a  22824  hstrlem3a  22832  mdbr3  22869  mdbr4  22870  dmdmd  22872  dmdbr3  22877  dmdbr4  22878  dmdbr5  22880  ssmd2  22884  mdslmd1i  22901  mdsymlem7  22981  cdj1i  23005  cdj3lem2b  23009  ghomf1olem  23405  brbtwn2  23940  comppfsc  25706  trintALT  27925  lub0N  28646  hlrelat2  28859  snatpsubN  29206  pmaple  29217  pclclN  29347  pclfinN  29356  pclfinclN  29406  ltrneq2  29604  trlval2  29619  trlord  30025
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-nf 1537  df-ral 2549
  Copyright terms: Public domain W3C validator