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

Theorem rexlimiva 2624
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 2623 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   E.wrex 2510
This theorem is referenced by:  unon  4513  tfrlem16  6295  oawordeulem  6438  nneob  6536  ominf  6960  unfilem1  7006  pwfi  7035  fival  7050  elfi2  7052  fi0  7057  fiin  7059  finnum  7465  dif1card  7522  fseqenlem2  7536  dfac8alem  7540  alephfp  7619  cflim2  7773  isfin1-3  7896  fin67  7905  isfin7-2  7906  axdc3lem  7960  axdc3lem2  7961  iunfo  8045  iundom2g  8046  winainflem  8195  rankcf  8279  map2psrpr  8612  supsrlem  8613  1re  8717  00id  8867  addid1  8872  om2uzrani  10893  uzrdgfni  10899  wrdf  11296  rexanuz  11706  r19.2uz  11712  fsum2dlem  12110  fsumcom2  12114  0dvds  12423  ppttop  16576  epttop  16578  neips  16682  lmmo  16940  2ndctop  17005  2ndcsep  17017  fbncp  17366  fgcl  17405  filuni  17412  tgioo  18134  zcld  18151  elovolm  18666  nulmbl2  18726  ellimc3  19061  limcflf  19063  pilem3  19661  perfect  20302  2vmadivsum  20522  selberg3lem2  20539  selberg4  20542  pntrsumbnd2  20548  pntrlog2bndlem3  20560  pntrlog2bndlem4  20561  pntpbnd  20569  pnt3  20593  norm1exi  21659  nmcexi  22436  lnconi  22443  pjssdif1i  22585  stri  22667  hstri  22675  stcltrthi  22688  shatomici  22768  trpredlem1  23398  elno  23468  noreson  23481  axcontlem12  23777  axcont  23778  lvsovso  24792  clscnc  25176  cover2  25524  prtlem16  25903  rexzrexnn0  26051  isnumbasgrplem2  26435  dgraalem  26516  bnj1398  27753  bnj1498  27780
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 2513  df-rex 2514
  Copyright terms: Public domain W3C validator