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

Theorem ralrimdva 2604
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 2603 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 2516
This theorem is referenced by:  ralxfrd  4485  isoselem  5737  resixpfo  6787  findcard  7030  ordtypelem2  7167  alephinit  7655  isfin2-2  7878  axpre-sup  8724  nnsub  9717  ublbneg  10234  xralrple  10463  supxrunb1  10569  expnlbnd2  11163  faclbnd4lem4  11240  hashbc  11321  cau3lem  11768  limsupbnd2  11887  climrlim2  11951  climshftlem  11978  subcn2  11998  isercoll  12071  climsup  12073  serf0  12083  iseralt  12087  sqr2irr  12454  pclem  12818  prmpwdvds  12878  vdwlem10  12964  vdwlem13  12967  ramtlecl  12974  ramub  12987  ramcl  13003  iscatd  13502  clatleglb  14157  grpinveu  14443  issubg4  14565  gexdvds  14822  sylow2alem2  14856  obselocv  16555  tgcn  16909  tgcnp  16910  lmconst  16918  cncls2  16929  cncls  16930  cnntr  16931  lmss  16953  cnt0  17001  isnrm2  17013  isreg2  17032  cmpsublem  17053  cmpsub  17054  tgcmp  17055  islly2  17137  kgencn2  17179  txdis  17253  txlm  17269  kqt0lem  17354  isr0  17355  regr1lem2  17358  cmphaushmeo  17418  cfinufil  17550  ufilen  17552  flimopn  17597  fbflim2  17599  fclsnei  17641  fclsbas  17643  fclsrest  17646  flimfnfcls  17650  fclscmp  17652  ufilcmp  17654  isfcf  17656  fcfnei  17657  cnpfcf  17663  tsmsres  17753  tsmsxp  17764  blbas  17903  prdsbl  17964  metss  17981  metcnp3  18013  bndth  18383  lebnumii  18391  iscfil3  18626  iscmet3lem1  18644  equivcfil  18652  equivcau  18653  ellimc3  19156  lhop1  19288  dvfsumrlim  19305  ftc1lem6  19315  fta1g  19480  dgrco  19583  plydivex  19604  fta1  19615  vieta1  19619  ulmshftlem  19695  ulmcaulem  19698  mtest  19708  cxpcn3lem  20014  cxploglim  20199  ftalem3  20239  dchrisumlem3  20567  pntibnd  20669  ostth2lem2  20710  grpoinveu  20814  isgrp2d  20827  nmcvcn  21193  blocnilem  21307  ubthlem3  21376  htthlem  21422  spansni  22061  bra11  22613  fnmulcv  25016  fnemeet2  25648  fnejoin2  25650  incsequz2  25791  geomcau  25807  caushft  25809  sstotbnd2  25830  isbnd2  25839  totbndbnd  25845  ismtybndlem  25862  heibor  25877  glb0N  28513  atlatle  28640  cvlcvr1  28659  ltrnid  29454  ltrneq2  29467
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 2520
  Copyright terms: Public domain W3C validator