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

Theorem ralrimdv 2645
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 1609 . 2  |-  F/ x ph
2 nfv 1609 . 2  |-  F/ x ps
3 ralrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
41, 2, 3ralrimd 2644 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ralrimdva  2646  ralrimivv  2647  wefrc  4403  oneqmin  4612  tfrlem1  6407  abianfp  6487  nneneq  7060  cflm  7892  coflim  7903  isf32lem12  8006  axdc3lem2  8093  zorn2lem7  8145  axpre-sup  8807  infmrcl  9749  zmax  10329  zbtwnre  10330  supxrunb2  10655  fzrevral  10882  islss4  15735  topbas  16726  elcls3  16836  neips  16866  clslp  16895  subbascn  17000  cnpnei  17009  fgss2  17585  fbflim2  17688  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  metcnp3  18102  aalioulem3  19730  hial0  21697  hial02  21698  ococss  21888  lnopmi  22596  adjlnop  22682  pjss2coi  22760  pj3cor1i  22805  strlem3a  22848  hstrlem3a  22856  mdbr3  22893  mdbr4  22894  dmdmd  22896  dmdbr3  22901  dmdbr4  22902  dmdbr5  22904  ssmd2  22908  mdslmd1i  22925  mdsymlem7  23005  cdj1i  23029  cdj3lem2b  23033  ghomf1olem  24016  brbtwn2  24605  comppfsc  26410  trintALT  28973  lub0N  30001  hlrelat2  30214  snatpsubN  30561  pmaple  30572  pclclN  30702  pclfinN  30711  pclfinclN  30761  ltrneq2  30959  trlval2  30974  trlord  31380
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator