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

Theorem rexlimiva 2817
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 424 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2816 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  unon  4803  tfrlem16  6646  oawordeulem  6789  nneob  6887  ominf  7313  unfilem1  7363  pwfi  7394  fival  7409  elfi2  7411  fi0  7417  fiin  7419  finnum  7827  dif1card  7884  fseqenlem2  7898  dfac8alem  7902  alephfp  7981  cflim2  8135  isfin1-3  8258  fin67  8267  isfin7-2  8268  axdc3lem  8322  axdc3lem2  8323  iunfo  8406  iundom2g  8407  winainflem  8560  rankcf  8644  map2psrpr  8977  supsrlem  8978  1re  9082  00id  9233  addid1  9238  om2uzrani  11284  uzrdgfni  11290  wrdf  11725  rexanuz  12141  r19.2uz  12147  fsum2dlem  12546  fsumcom2  12550  0dvds  12862  ppttop  17063  epttop  17065  neips  17169  lmmo  17436  2ndctop  17502  2ndcsep  17514  fbncp  17863  fgcl  17902  filuni  17909  tgioo  18819  zcld  18836  elovolm  19363  nulmbl2  19423  ellimc3  19758  limcflf  19760  pilem3  20361  perfect  21007  2vmadivsum  21227  selberg3lem2  21244  selberg4  21247  pntrsumbnd2  21253  pntrlog2bndlem3  21265  pntrlog2bndlem4  21266  pntpbnd  21274  pnt3  21298  norm1exi  22744  nmcexi  23521  lnconi  23528  pjssdif1i  23670  stri  23752  hstri  23760  stcltrthi  23773  shatomici  23853  isrnmeas  24546  dya2iocucvr  24626  sxbrsigalem1  24627  fprod2dlem  25296  fprodcom2  25300  trpredlem1  25497  elno  25593  noreson  25607  axcontlem12  25906  axcont  25907  mblfinlem2  26235  ismblfin  26237  volsupnfl  26241  itg2addnclem  26246  itg2addnc  26249  cover2  26406  prtlem16  26709  rexzrexnn0  26855  isnumbasgrplem2  27237  dgraalem  27318  stirlinglem13  27802  stirlinglem14  27803  stirling  27805  modprm0  28194  bnj1398  29340  bnj1498  29367
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-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator