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

Theorem ralrimdva 2756
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 2755 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 2666
This theorem is referenced by:  ralxfrd  4696  isoselem  6020  resixpfo  7059  findcard  7306  ordtypelem2  7444  alephinit  7932  isfin2-2  8155  axpre-sup  9000  nnsub  9994  ublbneg  10516  xralrple  10747  supxrunb1  10854  expnlbnd2  11465  faclbnd4lem4  11542  hashbc  11657  cau3lem  12113  limsupbnd2  12232  climrlim2  12296  climshftlem  12323  subcn2  12343  isercoll  12416  climsup  12418  serf0  12429  iseralt  12433  incexclem  12571  sqr2irr  12803  pclem  13167  prmpwdvds  13227  vdwlem10  13313  vdwlem13  13316  ramtlecl  13323  ramub  13336  ramcl  13352  iscatd  13853  clatleglb  14508  grpinveu  14794  issubg4  14916  gexdvds  15173  sylow2alem2  15207  obselocv  16910  tgcn  17270  tgcnp  17271  lmconst  17279  cncls2  17291  cncls  17292  cnntr  17293  lmss  17316  cnt0  17364  isnrm2  17376  isreg2  17395  cmpsublem  17416  cmpsub  17417  tgcmp  17418  islly2  17500  kgencn2  17542  txdis  17617  txlm  17633  kqt0lem  17721  isr0  17722  regr1lem2  17725  cmphaushmeo  17785  cfinufil  17913  ufilen  17915  flimopn  17960  fbflim2  17962  fclsnei  18004  fclsbas  18006  fclsrest  18009  flimfnfcls  18013  fclscmp  18015  ufilcmp  18017  isfcf  18019  fcfnei  18020  cnpfcf  18026  tsmsres  18126  tsmsxp  18137  blbas  18413  prdsbl  18474  metss  18491  metcnp3  18523  bndth  18936  lebnumii  18944  iscfil3  19179  iscmet3lem1  19197  equivcfil  19205  equivcau  19206  ellimc3  19719  lhop1  19851  dvfsumrlim  19868  ftc1lem6  19878  fta1g  20043  dgrco  20146  plydivex  20167  fta1  20178  vieta1  20182  ulmshftlem  20258  ulmcaulem  20263  mtest  20273  cxpcn3lem  20584  cxploglim  20769  ftalem3  20810  dchrisumlem3  21138  pntibnd  21240  ostth2lem2  21281  grpoinveu  21763  isgrp2d  21776  nmcvcn  22144  blocnilem  22258  ubthlem3  22327  htthlem  22373  spansni  23012  bra11  23564  lmxrge0  24290  ftc1cnnc  26178  fnemeet2  26286  fnejoin2  26288  incsequz2  26343  geomcau  26355  caushft  26357  sstotbnd2  26373  isbnd2  26382  totbndbnd  26388  ismtybndlem  26405  heibor  26420  climinf  27599  ralbinrald  27844  glb0N  29676  atlatle  29803  cvlcvr1  29822  ltrnid  30617  ltrneq2  30630
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 2671
  Copyright terms: Public domain W3C validator