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

Theorem ralrimdva 2634
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 2633 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1685   A.wral 2544
This theorem is referenced by:  ralxfrd  4547  isoselem  5800  resixpfo  6850  findcard  7093  ordtypelem2  7230  alephinit  7718  isfin2-2  7941  axpre-sup  8787  nnsub  9780  ublbneg  10298  xralrple  10528  supxrunb1  10634  expnlbnd2  11228  faclbnd4lem4  11305  hashbc  11387  cau3lem  11834  limsupbnd2  11953  climrlim2  12017  climshftlem  12044  subcn2  12064  isercoll  12137  climsup  12139  serf0  12149  iseralt  12153  incexclem  12291  sqr2irr  12523  pclem  12887  prmpwdvds  12947  vdwlem10  13033  vdwlem13  13036  ramtlecl  13043  ramub  13056  ramcl  13072  iscatd  13571  clatleglb  14226  grpinveu  14512  issubg4  14634  gexdvds  14891  sylow2alem2  14925  obselocv  16624  tgcn  16978  tgcnp  16979  lmconst  16987  cncls2  16998  cncls  16999  cnntr  17000  lmss  17022  cnt0  17070  isnrm2  17082  isreg2  17101  cmpsublem  17122  cmpsub  17123  tgcmp  17124  islly2  17206  kgencn2  17248  txdis  17322  txlm  17338  kqt0lem  17423  isr0  17424  regr1lem2  17427  cmphaushmeo  17487  cfinufil  17619  ufilen  17621  flimopn  17666  fbflim2  17668  fclsnei  17710  fclsbas  17712  fclsrest  17715  flimfnfcls  17719  fclscmp  17721  ufilcmp  17723  isfcf  17725  fcfnei  17726  cnpfcf  17732  tsmsres  17822  tsmsxp  17833  blbas  17972  prdsbl  18033  metss  18050  metcnp3  18082  bndth  18452  lebnumii  18460  iscfil3  18695  iscmet3lem1  18713  equivcfil  18721  equivcau  18722  ellimc3  19225  lhop1  19357  dvfsumrlim  19374  ftc1lem6  19384  fta1g  19549  dgrco  19652  plydivex  19673  fta1  19684  vieta1  19688  ulmshftlem  19764  ulmcaulem  19767  mtest  19777  cxpcn3lem  20083  cxploglim  20268  ftalem3  20308  dchrisumlem3  20636  pntibnd  20738  ostth2lem2  20779  grpoinveu  20883  isgrp2d  20896  nmcvcn  21262  blocnilem  21376  ubthlem3  21445  htthlem  21491  spansni  22132  bra11  22684  fnmulcv  25095  fnemeet2  25727  fnejoin2  25729  incsequz2  25870  geomcau  25886  caushft  25888  sstotbnd2  25909  isbnd2  25918  totbndbnd  25924  ismtybndlem  25941  heibor  25956  climinf  27143  ralbinrald  27368  glb0N  28662  atlatle  28789  cvlcvr1  28808  ltrnid  29603  ltrneq2  29616
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 1636  ax-8 1644  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2549
  Copyright terms: Public domain W3C validator