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

Theorem reximi 2813
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 2811 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 2706
This theorem is referenced by:  r19.29d2r  2851  r19.40  2859  reu3  3124  2reu5  3142  ssiun  4133  iinss  4142  elunirnALT  6000  iiner  6976  erovlem  7000  xpf1o  7269  unbnn2  7364  scott0  7810  dfac2  8011  cflm  8130  alephsing  8156  numthcor  8374  zorng  8384  zornn0g  8385  ttukeyg  8397  uniimadom  8419  axgroth3  8706  qextlt  10789  qextle  10790  rexanre  12150  climi2  12305  climi0  12306  rlimres  12352  lo1res  12353  caurcvgr  12467  caurcvg2  12471  caucvgb  12473  vdwnnlem1  13363  efgrelexlemb  15382  eltg2b  17024  neiptopuni  17194  neiptopnei  17196  ordtbas2  17255  lmcvg  17326  cnprest  17353  lmcnp  17368  nrmsep2  17420  1stcfb  17508  islly2  17547  llycmpkgen  17584  txbas  17599  tx1stc  17682  cnextcn  18098  tmdcn2  18119  utoptop  18264  ucnima  18311  cfiluweak  18325  metrest  18554  metustOLD  18597  metust  18598  cfilucfilOLD  18599  cfilucfil  18600  metustblOLD  18610  metustbl  18611  xrhmeo  18971  cmetcaulem  19241  iundisj  19442  limcresi  19772  elply2  20115  aalioulem2  20250  ulmf  20298  2sqlem7  21154  pntrsumbnd  21260  usgra2edg1  21403  3v3e3cycl1  21631  grpoidval  21804  grporcan  21809  grpoinveu  21810  grpomndo  21934  iundisjf  24029  xlt2addrd  24124  xrofsup  24126  iundisjfi  24152  rhmdvdsr  24256  tpr2rico  24310  esumc  24446  esumfsup  24460  esumpcvgval  24468  hasheuni  24475  voliune  24585  volfiniune  24586  dya2icoseg2  24628  dya2iocnei  24632  dya2iocuni  24633  lgamucov2  24823  prodmolem2  25261  prodmo  25262  colinearex  25994  segcon2  26039  opnrebl2  26324  sdclem2  26446  heibor1lem  26518  2r19.29  26703  prtlem9  26713  prtlem11  26715  prter1  26728  prter2  26730  eldiophb  26815  rmxyelqirr  26973  hbtlem1  27304  hbtlem7  27306  stirlinglem13  27811  reuan  27934  2reu2rex  27937  cshword  28235  cshwsiun  28286  1to3vfriendship  28398  2pthfrgrarn  28399  bnj31  29084  bnj1239  29177  bnj900  29300  bnj906  29301  bnj1398  29403  bnj1498  29430  hl2at  30202  cvrval4N  30211  athgt  30253  1dimN  30268  lhpexnle  30803  lhpexle1  30805  cdlemftr2  31363  cdlemftr1  31364  cdlemftr0  31365  cdlemg5  31402  cdlemg33c0  31499  mapdrvallem2  32443
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 2710  df-rex 2711
  Copyright terms: Public domain W3C validator