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

Theorem reximi 2773
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 2771 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   E.wrex 2667
This theorem is referenced by:  r19.29d2r  2811  r19.40  2819  reu3  3084  2reu5  3102  ssiun  4093  iinss  4102  elunirnALT  5959  iiner  6935  erovlem  6959  xpf1o  7228  unbnn2  7323  scott0  7766  dfac2  7967  cflm  8086  alephsing  8112  numthcor  8330  zorng  8340  zornn0g  8341  ttukeyg  8353  uniimadom  8375  axgroth3  8662  qextlt  10745  qextle  10746  rexanre  12105  climi2  12260  climi0  12261  rlimres  12307  lo1res  12308  caurcvgr  12422  caurcvg2  12426  caucvgb  12428  vdwnnlem1  13318  efgrelexlemb  15337  eltg2b  16979  neiptopuni  17149  neiptopnei  17151  ordtbas2  17209  lmcvg  17280  cnprest  17307  lmcnp  17322  nrmsep2  17374  1stcfb  17461  islly2  17500  llycmpkgen  17537  txbas  17552  tx1stc  17635  cnextcn  18051  tmdcn2  18072  utoptop  18217  ucnima  18264  cfiluweak  18278  metrest  18507  metustOLD  18550  metust  18551  cfilucfilOLD  18552  cfilucfil  18553  metustblOLD  18563  metustbl  18564  xrhmeo  18924  cmetcaulem  19194  iundisj  19395  limcresi  19725  elply2  20068  aalioulem2  20203  ulmf  20251  2sqlem7  21107  pntrsumbnd  21213  usgra2edg1  21356  3v3e3cycl1  21584  grpoidval  21757  grporcan  21762  grpoinveu  21763  grpomndo  21887  iundisjf  23982  xlt2addrd  24077  xrofsup  24079  iundisjfi  24105  rhmdvdsr  24209  tpr2rico  24263  esumc  24399  esumfsup  24413  esumpcvgval  24421  hasheuni  24428  voliune  24538  volfiniune  24539  dya2icoseg2  24581  dya2iocnei  24585  dya2iocuni  24586  lgamucov2  24776  prodmolem2  25214  prodmo  25215  colinearex  25898  segcon2  25943  opnrebl2  26214  sdclem2  26336  heibor1lem  26408  2r19.29  26593  prtlem9  26603  prtlem11  26605  prter1  26618  prter2  26620  eldiophb  26705  rmxyelqirr  26863  hbtlem1  27195  hbtlem7  27197  stirlinglem13  27702  reuan  27825  2reu2rex  27828  1to3vfriendship  28112  2pthfrgrarn  28113  bnj31  28790  bnj1239  28883  bnj900  29006  bnj906  29007  bnj1398  29109  bnj1498  29136  hl2at  29887  cvrval4N  29896  athgt  29938  1dimN  29953  lhpexnle  30488  lhpexle1  30490  cdlemftr2  31048  cdlemftr1  31049  cdlemftr0  31050  cdlemg5  31087  cdlemg33c0  31184  mapdrvallem2  32128
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator