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

Theorem ralrimdv 2800
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 1673 . 2  |-  F/ x ph
2 nfv 1673 . 2  |-  F/ x ps
3 ralrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
41, 2, 3ralrimd 2799 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   A.wral 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590  df-ral 2715
This theorem is referenced by:  ralrimdva  2801  ralrimivv  2802  wefrc  4709  oneqmin  6411  nneneq  7486  cflm  8411  coflim  8422  isf32lem12  8525  axdc3lem2  8612  zorn2lem7  8663  axpre-sup  9328  infmrcl  10301  zmax  10942  zbtwnre  10943  supxrunb2  11275  fzrevral  11536  islss4  17020  topbas  18552  elcls3  18662  neips  18692  clslp  18727  subbascn  18833  cnpnei  18843  fgss2  19422  fbflim2  19525  alexsubALTlem3  19596  alexsubALTlem4  19597  alexsubALT  19598  metcnp3  20090  aalioulem3  21775  brbtwn2  23102  hial0  24455  hial02  24456  ococss  24647  lnopmi  25355  adjlnop  25441  pjss2coi  25519  pj3cor1i  25564  strlem3a  25607  hstrlem3a  25615  mdbr3  25652  mdbr4  25653  dmdmd  25655  dmdbr3  25660  dmdbr4  25661  dmdbr5  25663  ssmd2  25667  mdslmd1i  25684  mdsymlem7  25764  cdj1i  25788  cdj3lem2b  25792  ghomf1olem  27264  comppfsc  28532  lindslinindsimp2  30886  trintALT  31504  lub0N  32674  glb0N  32678  hlrelat2  32887  snatpsubN  33234  pmaple  33245  pclclN  33375  pclfinN  33384  pclfinclN  33434  ltrneq2  33632  trlval2  33647  trlord  34053
  Copyright terms: Public domain W3C validator