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

Theorem ralrimdva 2783
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 2782 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   A.wral 2692
This theorem is referenced by:  ralxfrd  4723  isoselem  6047  resixpfo  7086  findcard  7333  ordtypelem2  7472  alephinit  7960  isfin2-2  8183  axpre-sup  9028  nnsub  10022  ublbneg  10544  xralrple  10775  supxrunb1  10882  expnlbnd2  11493  faclbnd4lem4  11570  hashbc  11685  cau3lem  12141  limsupbnd2  12260  climrlim2  12324  climshftlem  12351  subcn2  12371  isercoll  12444  climsup  12446  serf0  12457  iseralt  12461  incexclem  12599  sqr2irr  12831  pclem  13195  prmpwdvds  13255  vdwlem10  13341  vdwlem13  13344  ramtlecl  13351  ramub  13364  ramcl  13380  iscatd  13881  clatleglb  14536  grpinveu  14822  issubg4  14944  gexdvds  15201  sylow2alem2  15235  obselocv  16938  tgcn  17299  tgcnp  17300  lmconst  17308  cncls2  17320  cncls  17321  cnntr  17322  lmss  17345  cnt0  17393  isnrm2  17405  isreg2  17424  cmpsublem  17445  cmpsub  17446  tgcmp  17447  islly2  17530  kgencn2  17572  txdis  17647  txlm  17663  kqt0lem  17751  isr0  17752  regr1lem2  17755  cmphaushmeo  17815  cfinufil  17943  ufilen  17945  flimopn  17990  fbflim2  17992  fclsnei  18034  fclsbas  18036  fclsrest  18039  flimfnfcls  18043  fclscmp  18045  ufilcmp  18047  isfcf  18049  fcfnei  18050  cnpfcf  18056  tsmsres  18156  tsmsxp  18167  blbas  18443  prdsbl  18504  metss  18521  metcnp3  18553  bndth  18966  lebnumii  18974  iscfil3  19209  iscmet3lem1  19227  equivcfil  19235  equivcau  19236  ellimc3  19749  lhop1  19881  dvfsumrlim  19898  ftc1lem6  19908  fta1g  20073  dgrco  20176  plydivex  20197  fta1  20208  vieta1  20212  ulmshftlem  20288  ulmcaulem  20293  mtest  20303  cxpcn3lem  20614  cxploglim  20799  ftalem3  20840  dchrisumlem3  21168  pntibnd  21270  ostth2lem2  21311  grpoinveu  21793  isgrp2d  21806  nmcvcn  22174  blocnilem  22288  ubthlem3  22357  htthlem  22403  spansni  23042  bra11  23594  lmxrge0  24320  ftc1cnnc  26220  fnemeet2  26328  fnejoin2  26330  incsequz2  26385  geomcau  26397  caushft  26399  sstotbnd2  26415  isbnd2  26424  totbndbnd  26430  ismtybndlem  26447  heibor  26462  climinf  27641  ralbinrald  27886  glb0N  29722  atlatle  29849  cvlcvr1  29868  ltrnid  30663  ltrneq2  30676
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2697
  Copyright terms: Public domain W3C validator