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

Theorem rexlimiva 2662
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)
Hypothesis
Ref Expression
rexlimiva.1  |-  ( ( x  e.  A  /\  ph )  ->  ps )
Assertion
Ref Expression
rexlimiva  |-  ( E. x  e.  A  ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem rexlimiva
StepHypRef Expression
1 rexlimiva.1 . . 3  |-  ( ( x  e.  A  /\  ph )  ->  ps )
21ex 423 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2661 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  unon  4622  tfrlem16  6409  oawordeulem  6552  nneob  6650  ominf  7075  unfilem1  7121  pwfi  7151  fival  7166  elfi2  7168  fi0  7173  fiin  7175  finnum  7581  dif1card  7638  fseqenlem2  7652  dfac8alem  7656  alephfp  7735  cflim2  7889  isfin1-3  8012  fin67  8021  isfin7-2  8022  axdc3lem  8076  axdc3lem2  8077  iunfo  8161  iundom2g  8162  winainflem  8315  rankcf  8399  map2psrpr  8732  supsrlem  8733  1re  8837  00id  8987  addid1  8992  om2uzrani  11015  uzrdgfni  11021  wrdf  11419  rexanuz  11829  r19.2uz  11835  fsum2dlem  12233  fsumcom2  12237  0dvds  12549  ppttop  16744  epttop  16746  neips  16850  lmmo  17108  2ndctop  17173  2ndcsep  17185  fbncp  17534  fgcl  17573  filuni  17580  tgioo  18302  zcld  18319  elovolm  18834  nulmbl2  18894  ellimc3  19229  limcflf  19231  pilem3  19829  perfect  20470  2vmadivsum  20690  selberg3lem2  20707  selberg4  20710  pntrsumbnd2  20716  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntpbnd  20737  pnt3  20761  norm1exi  21829  nmcexi  22606  lnconi  22613  pjssdif1i  22755  stri  22837  hstri  22845  stcltrthi  22858  shatomici  22938  trpredlem1  23641  elno  23711  noreson  23725  axcontlem12  24014  axcont  24015  lvsovso  25038  clscnc  25422  cover2  25770  prtlem16  26149  rexzrexnn0  26297  isnumbasgrplem2  26681  dgraalem  26762  bnj1398  28437  bnj1498  28464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator