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

Theorem ralrimdv 2909
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 1674 . 2  |-  F/ x ph
2 nfv 1674 . 2  |-  F/ x ps
3 ralrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
41, 2, 3ralrimd 2908 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   A.wral 2798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591  df-ral 2803
This theorem is referenced by:  ralrimdva  2910  ralrimivv  2911  wefrc  4821  oneqmin  6525  nneneq  7603  cflm  8529  coflim  8540  isf32lem12  8643  axdc3lem2  8730  zorn2lem7  8781  axpre-sup  9446  infmrcl  10419  zmax  11060  zbtwnre  11061  supxrunb2  11393  fzrevral  11660  islss4  17165  topbas  18708  elcls3  18818  neips  18848  clslp  18883  subbascn  18989  cnpnei  18999  fgss2  19578  fbflim2  19681  alexsubALTlem3  19752  alexsubALTlem4  19753  alexsubALT  19754  metcnp3  20246  aalioulem3  21932  brbtwn2  23302  hial0  24655  hial02  24656  ococss  24847  lnopmi  25555  adjlnop  25641  pjss2coi  25719  pj3cor1i  25764  strlem3a  25807  hstrlem3a  25815  mdbr3  25852  mdbr4  25853  dmdmd  25855  dmdbr3  25860  dmdbr4  25861  dmdbr5  25863  ssmd2  25867  mdslmd1i  25884  mdsymlem7  25964  cdj1i  25988  cdj3lem2b  25992  ghomf1olem  27456  comppfsc  28726  lindslinindsimp2  31115  trintALT  31934  lub0N  33157  glb0N  33161  hlrelat2  33370  snatpsubN  33717  pmaple  33728  pclclN  33858  pclfinN  33867  pclfinclN  33917  ltrneq2  34115  trlval2  34130  trlord  34536
  Copyright terms: Public domain W3C validator