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

Theorem rexlimiva 2633
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 425 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2632 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  unon  4559  tfrlem16  6342  oawordeulem  6485  nneob  6583  ominf  7008  unfilem1  7054  pwfi  7084  fival  7099  elfi2  7101  fi0  7106  fiin  7108  finnum  7514  dif1card  7571  fseqenlem2  7585  dfac8alem  7589  alephfp  7668  cflim2  7822  isfin1-3  7945  fin67  7954  isfin7-2  7955  axdc3lem  8009  axdc3lem2  8010  iunfo  8094  iundom2g  8095  winainflem  8248  rankcf  8332  map2psrpr  8665  supsrlem  8666  1re  8770  00id  8920  addid1  8925  om2uzrani  10946  uzrdgfni  10952  wrdf  11349  rexanuz  11759  r19.2uz  11765  fsum2dlem  12163  fsumcom2  12167  0dvds  12476  ppttop  16671  epttop  16673  neips  16777  lmmo  17035  2ndctop  17100  2ndcsep  17112  fbncp  17461  fgcl  17500  filuni  17507  tgioo  18229  zcld  18246  elovolm  18761  nulmbl2  18821  ellimc3  19156  limcflf  19158  pilem3  19756  perfect  20397  2vmadivsum  20617  selberg3lem2  20634  selberg4  20637  pntrsumbnd2  20643  pntrlog2bndlem3  20655  pntrlog2bndlem4  20656  pntpbnd  20664  pnt3  20688  norm1exi  21754  nmcexi  22531  lnconi  22538  pjssdif1i  22680  stri  22762  hstri  22770  stcltrthi  22783  shatomici  22863  trpredlem1  23564  elno  23634  noreson  23647  axcontlem12  23943  axcont  23944  lvsovso  24958  clscnc  25342  cover2  25690  prtlem16  26069  rexzrexnn0  26217  isnumbasgrplem2  26601  dgraalem  26682  bnj1398  28076  bnj1498  28103
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2520  df-rex 2521
  Copyright terms: Public domain W3C validator