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

Theorem reximi 2805
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
Hypothesis
Ref Expression
reximi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
reximi  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )

Proof of Theorem reximi
StepHypRef Expression
1 reximi.1 . . 3  |-  ( ph  ->  ps )
21a1i 11 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32reximia 2803 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  r19.29d2r  2843  r19.40  2851  reu3  3116  2reu5  3134  ssiun  4125  iinss  4134  elunirnALT  5992  iiner  6968  erovlem  6992  xpf1o  7261  unbnn2  7356  scott0  7802  dfac2  8003  cflm  8122  alephsing  8148  numthcor  8366  zorng  8376  zornn0g  8377  ttukeyg  8389  uniimadom  8411  axgroth3  8698  qextlt  10781  qextle  10782  rexanre  12142  climi2  12297  climi0  12298  rlimres  12344  lo1res  12345  caurcvgr  12459  caurcvg2  12463  caucvgb  12465  vdwnnlem1  13355  efgrelexlemb  15374  eltg2b  17016  neiptopuni  17186  neiptopnei  17188  ordtbas2  17247  lmcvg  17318  cnprest  17345  lmcnp  17360  nrmsep2  17412  1stcfb  17500  islly2  17539  llycmpkgen  17576  txbas  17591  tx1stc  17674  cnextcn  18090  tmdcn2  18111  utoptop  18256  ucnima  18303  cfiluweak  18317  metrest  18546  metustOLD  18589  metust  18590  cfilucfilOLD  18591  cfilucfil  18592  metustblOLD  18602  metustbl  18603  xrhmeo  18963  cmetcaulem  19233  iundisj  19434  limcresi  19764  elply2  20107  aalioulem2  20242  ulmf  20290  2sqlem7  21146  pntrsumbnd  21252  usgra2edg1  21395  3v3e3cycl1  21623  grpoidval  21796  grporcan  21801  grpoinveu  21802  grpomndo  21926  iundisjf  24021  xlt2addrd  24116  xrofsup  24118  iundisjfi  24144  rhmdvdsr  24248  tpr2rico  24302  esumc  24438  esumfsup  24452  esumpcvgval  24460  hasheuni  24467  voliune  24577  volfiniune  24578  dya2icoseg2  24620  dya2iocnei  24624  dya2iocuni  24625  lgamucov2  24815  prodmolem2  25253  prodmo  25254  colinearex  25986  segcon2  26031  opnrebl2  26315  sdclem2  26437  heibor1lem  26509  2r19.29  26694  prtlem9  26704  prtlem11  26706  prter1  26719  prter2  26721  eldiophb  26806  rmxyelqirr  26964  hbtlem1  27295  hbtlem7  27297  stirlinglem13  27802  reuan  27925  2reu2rex  27928  cshword  28201  cshwsiun  28249  1to3vfriendship  28335  2pthfrgrarn  28336  bnj31  29021  bnj1239  29114  bnj900  29237  bnj906  29238  bnj1398  29340  bnj1498  29367  hl2at  30139  cvrval4N  30148  athgt  30190  1dimN  30205  lhpexnle  30740  lhpexle1  30742  cdlemftr2  31300  cdlemftr1  31301  cdlemftr0  31302  cdlemg5  31339  cdlemg33c0  31436  mapdrvallem2  32380
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator