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

Theorem ralrimdva 2633
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)
Hypothesis
Ref Expression
ralrimdva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ralrimdva  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Distinct variable groups:    ph, x    ps, x
Allowed substitution hints:    ch( x)    A( x)

Proof of Theorem ralrimdva
StepHypRef Expression
1 ralrimdva.1 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
21ex 423 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32com23 72 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
43ralrimdv 2632 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralxfrd  4548  isoselem  5838  resixpfo  6854  findcard  7097  ordtypelem2  7234  alephinit  7722  isfin2-2  7945  axpre-sup  8791  nnsub  9784  ublbneg  10302  xralrple  10532  supxrunb1  10638  expnlbnd2  11232  faclbnd4lem4  11309  hashbc  11391  cau3lem  11838  limsupbnd2  11957  climrlim2  12021  climshftlem  12048  subcn2  12068  isercoll  12141  climsup  12143  serf0  12153  iseralt  12157  incexclem  12295  sqr2irr  12527  pclem  12891  prmpwdvds  12951  vdwlem10  13037  vdwlem13  13040  ramtlecl  13047  ramub  13060  ramcl  13076  iscatd  13575  clatleglb  14230  grpinveu  14516  issubg4  14638  gexdvds  14895  sylow2alem2  14929  obselocv  16628  tgcn  16982  tgcnp  16983  lmconst  16991  cncls2  17002  cncls  17003  cnntr  17004  lmss  17026  cnt0  17074  isnrm2  17086  isreg2  17105  cmpsublem  17126  cmpsub  17127  tgcmp  17128  islly2  17210  kgencn2  17252  txdis  17326  txlm  17342  kqt0lem  17427  isr0  17428  regr1lem2  17431  cmphaushmeo  17491  cfinufil  17623  ufilen  17625  flimopn  17670  fbflim2  17672  fclsnei  17714  fclsbas  17716  fclsrest  17719  flimfnfcls  17723  fclscmp  17725  ufilcmp  17727  isfcf  17729  fcfnei  17730  cnpfcf  17736  tsmsres  17826  tsmsxp  17837  blbas  17976  prdsbl  18037  metss  18054  metcnp3  18086  bndth  18456  lebnumii  18464  iscfil3  18699  iscmet3lem1  18717  equivcfil  18725  equivcau  18726  ellimc3  19229  lhop1  19361  dvfsumrlim  19378  ftc1lem6  19388  fta1g  19553  dgrco  19656  plydivex  19677  fta1  19688  vieta1  19692  ulmshftlem  19768  ulmcaulem  19771  mtest  19781  cxpcn3lem  20087  cxploglim  20272  ftalem3  20312  dchrisumlem3  20640  pntibnd  20742  ostth2lem2  20783  grpoinveu  20889  isgrp2d  20902  nmcvcn  21268  blocnilem  21382  ubthlem3  21451  htthlem  21497  spansni  22136  bra11  22688  lmxrge0  23375  fnmulcv  25684  fnemeet2  26316  fnejoin2  26318  incsequz2  26459  geomcau  26475  caushft  26477  sstotbnd2  26498  isbnd2  26507  totbndbnd  26513  ismtybndlem  26530  heibor  26545  climinf  27732  ralbinrald  27977  glb0N  29383  atlatle  29510  cvlcvr1  29529  ltrnid  30324  ltrneq2  30337
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator