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

Theorem ralrimdva 2595
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 425 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32com23 74 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
43ralrimdv 2594 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   A.wral 2509
This theorem is referenced by:  ralxfrd  4439  isoselem  5690  resixpfo  6740  findcard  6982  ordtypelem2  7118  alephinit  7606  isfin2-2  7829  axpre-sup  8671  nnsub  9664  ublbneg  10181  xralrple  10410  supxrunb1  10516  expnlbnd2  11110  faclbnd4lem4  11187  hashbc  11268  cau3lem  11715  limsupbnd2  11834  climrlim2  11898  climshftlem  11925  subcn2  11945  isercoll  12018  climsup  12020  serf0  12030  iseralt  12034  sqr2irr  12401  pclem  12765  prmpwdvds  12825  vdwlem10  12911  vdwlem13  12914  ramtlecl  12921  ramub  12934  ramcl  12950  iscatd  13419  clatleglb  14074  grpinveu  14351  issubg4  14473  gexdvds  14730  sylow2alem2  14764  obselocv  16460  tgcn  16814  tgcnp  16815  lmconst  16823  cncls2  16834  cncls  16835  cnntr  16836  lmss  16858  cnt0  16906  isnrm2  16918  isreg2  16937  cmpsublem  16958  cmpsub  16959  tgcmp  16960  islly2  17042  kgencn2  17084  txdis  17158  txlm  17174  kqt0lem  17259  isr0  17260  regr1lem2  17263  cmphaushmeo  17323  cfinufil  17455  ufilen  17457  flimopn  17502  fbflim2  17504  fclsnei  17546  fclsbas  17548  fclsrest  17551  flimfnfcls  17555  fclscmp  17557  ufilcmp  17559  isfcf  17561  fcfnei  17562  cnpfcf  17568  tsmsres  17658  tsmsxp  17669  blbas  17808  prdsbl  17869  metss  17886  metcnp3  17918  bndth  18288  lebnumii  18296  iscfil3  18531  iscmet3lem1  18549  equivcfil  18557  equivcau  18558  ellimc3  19061  lhop1  19193  dvfsumrlim  19210  ftc1lem6  19220  fta1g  19385  dgrco  19488  plydivex  19509  fta1  19520  vieta1  19524  ulmshftlem  19600  ulmcaulem  19603  mtest  19613  cxpcn3lem  19955  cxploglim  20104  ftalem3  20144  dchrisumlem3  20472  pntibnd  20574  ostth2lem2  20615  grpoinveu  20719  isgrp2d  20732  nmcvcn  21098  blocnilem  21212  ubthlem3  21281  htthlem  21327  spansni  21966  bra11  22518  fnmulcv  24850  fnemeet2  25482  fnejoin2  25484  incsequz2  25625  geomcau  25641  caushft  25643  sstotbnd2  25664  isbnd2  25673  totbndbnd  25679  ismtybndlem  25696  heibor  25711  glb0N  28072  atlatle  28199  cvlcvr1  28218  ltrnid  29013  ltrneq2  29026
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-ral 2513
  Copyright terms: Public domain W3C validator