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

Theorem ralrimdva 2760
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 424 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32com23 74 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
43ralrimdv 2759 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   A.wral 2670
This theorem is referenced by:  ralxfrd  4700  isoselem  6024  resixpfo  7063  findcard  7310  ordtypelem2  7448  alephinit  7936  isfin2-2  8159  axpre-sup  9004  nnsub  9998  ublbneg  10520  xralrple  10751  supxrunb1  10858  expnlbnd2  11469  faclbnd4lem4  11546  hashbc  11661  cau3lem  12117  limsupbnd2  12236  climrlim2  12300  climshftlem  12327  subcn2  12347  isercoll  12420  climsup  12422  serf0  12433  iseralt  12437  incexclem  12575  sqr2irr  12807  pclem  13171  prmpwdvds  13231  vdwlem10  13317  vdwlem13  13320  ramtlecl  13327  ramub  13340  ramcl  13356  iscatd  13857  clatleglb  14512  grpinveu  14798  issubg4  14920  gexdvds  15177  sylow2alem2  15211  obselocv  16914  tgcn  17274  tgcnp  17275  lmconst  17283  cncls2  17295  cncls  17296  cnntr  17297  lmss  17320  cnt0  17368  isnrm2  17380  isreg2  17399  cmpsublem  17420  cmpsub  17421  tgcmp  17422  islly2  17504  kgencn2  17546  txdis  17621  txlm  17637  kqt0lem  17725  isr0  17726  regr1lem2  17729  cmphaushmeo  17789  cfinufil  17917  ufilen  17919  flimopn  17964  fbflim2  17966  fclsnei  18008  fclsbas  18010  fclsrest  18013  flimfnfcls  18017  fclscmp  18019  ufilcmp  18021  isfcf  18023  fcfnei  18024  cnpfcf  18030  tsmsres  18130  tsmsxp  18141  blbas  18417  prdsbl  18478  metss  18495  metcnp3  18527  bndth  18940  lebnumii  18948  iscfil3  19183  iscmet3lem1  19201  equivcfil  19209  equivcau  19210  ellimc3  19723  lhop1  19855  dvfsumrlim  19872  ftc1lem6  19882  fta1g  20047  dgrco  20150  plydivex  20171  fta1  20182  vieta1  20186  ulmshftlem  20262  ulmcaulem  20267  mtest  20277  cxpcn3lem  20588  cxploglim  20773  ftalem3  20814  dchrisumlem3  21142  pntibnd  21244  ostth2lem2  21285  grpoinveu  21767  isgrp2d  21780  nmcvcn  22148  blocnilem  22262  ubthlem3  22331  htthlem  22377  spansni  23016  bra11  23568  lmxrge0  24294  ftc1cnnc  26182  fnemeet2  26290  fnejoin2  26292  incsequz2  26347  geomcau  26359  caushft  26361  sstotbnd2  26377  isbnd2  26386  totbndbnd  26392  ismtybndlem  26409  heibor  26424  climinf  27603  ralbinrald  27848  glb0N  29680  atlatle  29807  cvlcvr1  29826  ltrnid  30621  ltrneq2  30634
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2675
  Copyright terms: Public domain W3C validator