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

Theorem rexlimiva 2675
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 2674 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  unon  4638  tfrlem16  6425  oawordeulem  6568  nneob  6666  ominf  7091  unfilem1  7137  pwfi  7167  fival  7182  elfi2  7184  fi0  7189  fiin  7191  finnum  7597  dif1card  7654  fseqenlem2  7668  dfac8alem  7672  alephfp  7751  cflim2  7905  isfin1-3  8028  fin67  8037  isfin7-2  8038  axdc3lem  8092  axdc3lem2  8093  iunfo  8177  iundom2g  8178  winainflem  8331  rankcf  8415  map2psrpr  8748  supsrlem  8749  1re  8853  00id  9003  addid1  9008  om2uzrani  11031  uzrdgfni  11037  wrdf  11435  rexanuz  11845  r19.2uz  11851  fsum2dlem  12249  fsumcom2  12253  0dvds  12565  ppttop  16760  epttop  16762  neips  16866  lmmo  17124  2ndctop  17189  2ndcsep  17201  fbncp  17550  fgcl  17589  filuni  17596  tgioo  18318  zcld  18335  elovolm  18850  nulmbl2  18910  ellimc3  19245  limcflf  19247  pilem3  19845  perfect  20486  2vmadivsum  20706  selberg3lem2  20723  selberg4  20726  pntrsumbnd2  20732  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntpbnd  20753  pnt3  20777  norm1exi  21845  nmcexi  22622  lnconi  22629  pjssdif1i  22771  stri  22853  hstri  22861  stcltrthi  22874  shatomici  22954  dya2iocct  23596  trpredlem1  24301  elno  24371  noreson  24385  axcontlem12  24675  axcont  24676  itg2addnclem  25003  itg2addnc  25005  lvsovso  25729  clscnc  26113  cover2  26461  prtlem16  26840  rexzrexnn0  26988  isnumbasgrplem2  27372  dgraalem  27453  bnj1398  29380  bnj1498  29407
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator