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

Theorem ralrimdva 2608
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 2607 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 2518
This theorem is referenced by:  ralxfrd  4520  isoselem  5772  resixpfo  6822  findcard  7065  ordtypelem2  7202  alephinit  7690  isfin2-2  7913  axpre-sup  8759  nnsub  9752  ublbneg  10270  xralrple  10499  supxrunb1  10605  expnlbnd2  11199  faclbnd4lem4  11276  hashbc  11357  cau3lem  11804  limsupbnd2  11923  climrlim2  11987  climshftlem  12014  subcn2  12034  isercoll  12107  climsup  12109  serf0  12119  iseralt  12123  sqr2irr  12490  pclem  12854  prmpwdvds  12914  vdwlem10  13000  vdwlem13  13003  ramtlecl  13010  ramub  13023  ramcl  13039  iscatd  13538  clatleglb  14193  grpinveu  14479  issubg4  14601  gexdvds  14858  sylow2alem2  14892  obselocv  16591  tgcn  16945  tgcnp  16946  lmconst  16954  cncls2  16965  cncls  16966  cnntr  16967  lmss  16989  cnt0  17037  isnrm2  17049  isreg2  17068  cmpsublem  17089  cmpsub  17090  tgcmp  17091  islly2  17173  kgencn2  17215  txdis  17289  txlm  17305  kqt0lem  17390  isr0  17391  regr1lem2  17394  cmphaushmeo  17454  cfinufil  17586  ufilen  17588  flimopn  17633  fbflim2  17635  fclsnei  17677  fclsbas  17679  fclsrest  17682  flimfnfcls  17686  fclscmp  17688  ufilcmp  17690  isfcf  17692  fcfnei  17693  cnpfcf  17699  tsmsres  17789  tsmsxp  17800  blbas  17939  prdsbl  18000  metss  18017  metcnp3  18049  bndth  18419  lebnumii  18427  iscfil3  18662  iscmet3lem1  18680  equivcfil  18688  equivcau  18689  ellimc3  19192  lhop1  19324  dvfsumrlim  19341  ftc1lem6  19351  fta1g  19516  dgrco  19619  plydivex  19640  fta1  19651  vieta1  19655  ulmshftlem  19731  ulmcaulem  19734  mtest  19744  cxpcn3lem  20050  cxploglim  20235  ftalem3  20275  dchrisumlem3  20603  pntibnd  20705  ostth2lem2  20746  grpoinveu  20850  isgrp2d  20863  nmcvcn  21229  blocnilem  21343  ubthlem3  21412  htthlem  21458  spansni  22097  bra11  22649  fnmulcv  25052  fnemeet2  25684  fnejoin2  25686  incsequz2  25827  geomcau  25843  caushft  25845  sstotbnd2  25866  isbnd2  25875  totbndbnd  25881  ismtybndlem  25898  heibor  25913  climinf  27101  glb0N  28633  atlatle  28760  cvlcvr1  28779  ltrnid  29574  ltrneq2  29587
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 2523
  Copyright terms: Public domain W3C validator