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

Theorem ralrimdva 2709
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 2708 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1710   A.wral 2619
This theorem is referenced by:  ralxfrd  4630  isoselem  5925  resixpfo  6942  findcard  7187  ordtypelem2  7324  alephinit  7812  isfin2-2  8035  axpre-sup  8881  nnsub  9874  ublbneg  10394  xralrple  10624  supxrunb1  10730  expnlbnd2  11325  faclbnd4lem4  11402  hashbc  11487  cau3lem  11934  limsupbnd2  12053  climrlim2  12117  climshftlem  12144  subcn2  12164  isercoll  12237  climsup  12239  serf0  12250  iseralt  12254  incexclem  12392  sqr2irr  12624  pclem  12988  prmpwdvds  13048  vdwlem10  13134  vdwlem13  13137  ramtlecl  13144  ramub  13157  ramcl  13173  iscatd  13674  clatleglb  14329  grpinveu  14615  issubg4  14737  gexdvds  14994  sylow2alem2  15028  obselocv  16734  tgcn  17088  tgcnp  17089  lmconst  17097  cncls2  17108  cncls  17109  cnntr  17110  lmss  17132  cnt0  17180  isnrm2  17192  isreg2  17211  cmpsublem  17232  cmpsub  17233  tgcmp  17234  islly2  17316  kgencn2  17358  txdis  17432  txlm  17448  kqt0lem  17533  isr0  17534  regr1lem2  17537  cmphaushmeo  17597  cfinufil  17725  ufilen  17727  flimopn  17772  fbflim2  17774  fclsnei  17816  fclsbas  17818  fclsrest  17821  flimfnfcls  17825  fclscmp  17827  ufilcmp  17829  isfcf  17831  fcfnei  17832  cnpfcf  17838  tsmsres  17928  tsmsxp  17939  blbas  18078  prdsbl  18139  metss  18156  metcnp3  18188  bndth  18560  lebnumii  18568  iscfil3  18803  iscmet3lem1  18821  equivcfil  18829  equivcau  18830  ellimc3  19333  lhop1  19465  dvfsumrlim  19482  ftc1lem6  19492  fta1g  19657  dgrco  19760  plydivex  19781  fta1  19792  vieta1  19796  ulmshftlem  19872  ulmcaulem  19877  mtest  19887  cxpcn3lem  20198  cxploglim  20383  ftalem3  20424  dchrisumlem3  20752  pntibnd  20854  ostth2lem2  20895  grpoinveu  21001  isgrp2d  21014  nmcvcn  21382  blocnilem  21496  ubthlem3  21565  htthlem  21611  spansni  22250  bra11  22802  lmxrge0  23493  ftc1cnnc  25514  fnemeet2  25640  fnejoin2  25642  incsequz2  25783  geomcau  25799  caushft  25801  sstotbnd2  25821  isbnd2  25830  totbndbnd  25836  ismtybndlem  25853  heibor  25868  climinf  27055  ralbinrald  27300  glb0N  29452  atlatle  29579  cvlcvr1  29598  ltrnid  30393  ltrneq2  30406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2624
  Copyright terms: Public domain W3C validator