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

Theorem ralrimdv 2594
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 2593 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   A.wral 2509
This theorem is referenced by:  ralrimdva  2595  ralrimivv  2596  wefrc  4280  oneqmin  4487  tfrlem1  6277  abianfp  6357  nneneq  6929  cflm  7760  coflim  7771  isf32lem12  7874  axdc3lem2  7961  zorn2lem7  8013  axpre-sup  8671  infmrcl  9613  zmax  10192  zbtwnre  10193  supxrunb2  10517  fzrevral  10744  islss4  15554  topbas  16542  elcls3  16652  neips  16682  clslp  16711  subbascn  16816  cnpnei  16825  fgss2  17401  fbflim2  17504  alexsubALTlem3  17575  alexsubALTlem4  17576  alexsubALT  17577  metcnp3  17918  aalioulem3  19546  hial0  21511  hial02  21512  ococss  21702  lnopmi  22410  adjlnop  22496  pjss2coi  22574  pj3cor1i  22619  strlem3a  22662  hstrlem3a  22670  mdbr3  22707  mdbr4  22708  dmdmd  22710  dmdbr3  22715  dmdbr4  22716  dmdbr5  22718  ssmd2  22722  mdslmd1i  22739  mdsymlem7  22819  cdj1i  22843  cdj3lem2b  22847  ghomf1olem  23172  brbtwn2  23707  comppfsc  25473  trintALT  27347  lub0N  28068  hlrelat2  28281  snatpsubN  28628  pmaple  28639  pclclN  28769  pclfinN  28778  pclfinclN  28828  ltrneq2  29026  trlval2  29041  trlord  29447
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 2513
  Copyright terms: Public domain W3C validator