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

Theorem ralrimdva 2635
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 2634 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1686   A.wral 2545
This theorem is referenced by:  ralxfrd  4550  isoselem  5840  resixpfo  6856  findcard  7099  ordtypelem2  7236  alephinit  7724  isfin2-2  7947  axpre-sup  8793  nnsub  9786  ublbneg  10304  xralrple  10534  supxrunb1  10640  expnlbnd2  11234  faclbnd4lem4  11311  hashbc  11393  cau3lem  11840  limsupbnd2  11959  climrlim2  12023  climshftlem  12050  subcn2  12070  isercoll  12143  climsup  12145  serf0  12155  iseralt  12159  incexclem  12297  sqr2irr  12529  pclem  12893  prmpwdvds  12953  vdwlem10  13039  vdwlem13  13042  ramtlecl  13049  ramub  13062  ramcl  13078  iscatd  13577  clatleglb  14232  grpinveu  14518  issubg4  14640  gexdvds  14897  sylow2alem2  14931  obselocv  16630  tgcn  16984  tgcnp  16985  lmconst  16993  cncls2  17004  cncls  17005  cnntr  17006  lmss  17028  cnt0  17076  isnrm2  17088  isreg2  17107  cmpsublem  17128  cmpsub  17129  tgcmp  17130  islly2  17212  kgencn2  17254  txdis  17328  txlm  17344  kqt0lem  17429  isr0  17430  regr1lem2  17433  cmphaushmeo  17493  cfinufil  17625  ufilen  17627  flimopn  17672  fbflim2  17674  fclsnei  17716  fclsbas  17718  fclsrest  17721  flimfnfcls  17725  fclscmp  17727  ufilcmp  17729  isfcf  17731  fcfnei  17732  cnpfcf  17738  tsmsres  17828  tsmsxp  17839  blbas  17978  prdsbl  18039  metss  18056  metcnp3  18088  bndth  18458  lebnumii  18466  iscfil3  18701  iscmet3lem1  18719  equivcfil  18727  equivcau  18728  ellimc3  19231  lhop1  19363  dvfsumrlim  19380  ftc1lem6  19390  fta1g  19555  dgrco  19658  plydivex  19679  fta1  19690  vieta1  19694  ulmshftlem  19770  ulmcaulem  19773  mtest  19783  cxpcn3lem  20089  cxploglim  20274  ftalem3  20314  dchrisumlem3  20642  pntibnd  20744  ostth2lem2  20785  grpoinveu  20891  isgrp2d  20904  nmcvcn  21270  blocnilem  21384  ubthlem3  21453  htthlem  21499  spansni  22138  bra11  22690  lmxrge0  23377  fnmulcv  25695  fnemeet2  26327  fnejoin2  26329  incsequz2  26470  geomcau  26486  caushft  26488  sstotbnd2  26509  isbnd2  26518  totbndbnd  26524  ismtybndlem  26541  heibor  26556  climinf  27743  ralbinrald  27988  glb0N  29456  atlatle  29583  cvlcvr1  29602  ltrnid  30397  ltrneq2  30410
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1534  df-ral 2550
  Copyright terms: Public domain W3C validator