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

Theorem rexlimiva 2664
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 2663 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1686   E.wrex 2546
This theorem is referenced by:  unon  4624  tfrlem16  6411  oawordeulem  6554  nneob  6652  ominf  7077  unfilem1  7123  pwfi  7153  fival  7168  elfi2  7170  fi0  7175  fiin  7177  finnum  7583  dif1card  7640  fseqenlem2  7654  dfac8alem  7658  alephfp  7737  cflim2  7891  isfin1-3  8014  fin67  8023  isfin7-2  8024  axdc3lem  8078  axdc3lem2  8079  iunfo  8163  iundom2g  8164  winainflem  8317  rankcf  8401  map2psrpr  8734  supsrlem  8735  1re  8839  00id  8989  addid1  8994  om2uzrani  11017  uzrdgfni  11023  wrdf  11421  rexanuz  11831  r19.2uz  11837  fsum2dlem  12235  fsumcom2  12239  0dvds  12551  ppttop  16746  epttop  16748  neips  16852  lmmo  17110  2ndctop  17175  2ndcsep  17187  fbncp  17536  fgcl  17575  filuni  17582  tgioo  18304  zcld  18321  elovolm  18836  nulmbl2  18896  ellimc3  19231  limcflf  19233  pilem3  19831  perfect  20472  2vmadivsum  20692  selberg3lem2  20709  selberg4  20712  pntrsumbnd2  20718  pntrlog2bndlem3  20730  pntrlog2bndlem4  20731  pntpbnd  20739  pnt3  20763  norm1exi  21831  nmcexi  22608  lnconi  22615  pjssdif1i  22757  stri  22839  hstri  22847  stcltrthi  22860  shatomici  22940  dya2iocct  23583  trpredlem1  24232  elno  24302  noreson  24316  axcontlem12  24605  axcont  24606  itg2addnclem  24933  itg2addnc  24935  lvsovso  25637  clscnc  26021  cover2  26369  prtlem16  26748  rexzrexnn0  26896  isnumbasgrplem2  27280  dgraalem  27361  bnj1398  29137  bnj1498  29164
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531  df-nf 1534  df-ral 2550  df-rex 2551
  Copyright terms: Public domain W3C validator