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

Theorem ralrimdv 2755
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 1626 . 2  |-  F/ x ph
2 nfv 1626 . 2  |-  F/ x ps
3 ralrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
41, 2, 3ralrimd 2754 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   A.wral 2666
This theorem is referenced by:  ralrimdva  2756  ralrimivv  2757  wefrc  4536  oneqmin  4744  tfrlem1  6595  abianfp  6675  nneneq  7249  cflm  8086  coflim  8097  isf32lem12  8200  axdc3lem2  8287  zorn2lem7  8338  axpre-sup  9000  infmrcl  9943  zmax  10527  zbtwnre  10528  supxrunb2  10855  fzrevral  11086  islss4  15993  topbas  16992  elcls3  17102  neips  17132  clslp  17166  subbascn  17272  cnpnei  17282  fgss2  17859  fbflim2  17962  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  metcnp3  18523  aalioulem3  20204  hial0  22557  hial02  22558  ococss  22748  lnopmi  23456  adjlnop  23542  pjss2coi  23620  pj3cor1i  23665  strlem3a  23708  hstrlem3a  23716  mdbr3  23753  mdbr4  23754  dmdmd  23756  dmdbr3  23761  dmdbr4  23762  dmdbr5  23764  ssmd2  23768  mdslmd1i  23785  mdsymlem7  23865  cdj1i  23889  cdj3lem2b  23893  ghomf1olem  25058  brbtwn2  25748  comppfsc  26277  trintALT  28702  lub0N  29672  hlrelat2  29885  snatpsubN  30232  pmaple  30243  pclclN  30373  pclfinN  30382  pclfinclN  30432  ltrneq2  30630  trlval2  30645  trlord  31051
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-ral 2671
  Copyright terms: Public domain W3C validator