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

Theorem rexlimiva 2637
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 2636 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   E.wrex 2519
This theorem is referenced by:  unon  4594  tfrlem16  6377  oawordeulem  6520  nneob  6618  ominf  7043  unfilem1  7089  pwfi  7119  fival  7134  elfi2  7136  fi0  7141  fiin  7143  finnum  7549  dif1card  7606  fseqenlem2  7620  dfac8alem  7624  alephfp  7703  cflim2  7857  isfin1-3  7980  fin67  7989  isfin7-2  7990  axdc3lem  8044  axdc3lem2  8045  iunfo  8129  iundom2g  8130  winainflem  8283  rankcf  8367  map2psrpr  8700  supsrlem  8701  1re  8805  00id  8955  addid1  8960  om2uzrani  10982  uzrdgfni  10988  wrdf  11385  rexanuz  11795  r19.2uz  11801  fsum2dlem  12199  fsumcom2  12203  0dvds  12512  ppttop  16707  epttop  16709  neips  16813  lmmo  17071  2ndctop  17136  2ndcsep  17148  fbncp  17497  fgcl  17536  filuni  17543  tgioo  18265  zcld  18282  elovolm  18797  nulmbl2  18857  ellimc3  19192  limcflf  19194  pilem3  19792  perfect  20433  2vmadivsum  20653  selberg3lem2  20670  selberg4  20673  pntrsumbnd2  20679  pntrlog2bndlem3  20691  pntrlog2bndlem4  20692  pntpbnd  20700  pnt3  20724  norm1exi  21790  nmcexi  22567  lnconi  22574  pjssdif1i  22716  stri  22798  hstri  22806  stcltrthi  22819  shatomici  22899  trpredlem1  23600  elno  23670  noreson  23683  axcontlem12  23979  axcont  23980  lvsovso  24994  clscnc  25378  cover2  25726  prtlem16  26105  rexzrexnn0  26253  isnumbasgrplem2  26637  dgraalem  26718  bnj1398  28196  bnj1498  28223
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 2523  df-rex 2524
  Copyright terms: Public domain W3C validator