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

Theorem reximi 2726
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 10 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32reximia 2724 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   E.wrex 2620
This theorem is referenced by:  r19.40  2767  reu3  3031  2reu5  3049  ssiun  4025  iinss  4034  elunirnALT  5866  iiner  6818  erovlem  6842  xpf1o  7111  unbnn2  7204  scott0  7646  dfac2  7847  cflm  7966  alephsing  7992  numthcor  8211  zorng  8221  zornn0g  8222  ttukeyg  8234  uniimadom  8256  axgroth3  8543  qextlt  10622  qextle  10623  rexanre  11926  climi2  12081  climi0  12082  rlimres  12128  lo1res  12129  caurcvgr  12243  caurcvg2  12247  caucvgb  12249  vdwnnlem1  13139  efgrelexlemb  15158  eltg2b  16803  ordtbas2  17027  lmcvg  17098  cnprest  17123  lmcnp  17138  nrmsep2  17190  1stcfb  17277  islly2  17316  llycmpkgen  17353  txbas  17368  tx1stc  17450  tmdcn2  17874  metrest  18172  xrhmeo  18548  cmetcaulem  18818  iundisj  19009  limcresi  19339  elply2  19682  aalioulem2  19817  ulmf  19865  2sqlem7  20721  pntrsumbnd  20827  grpoidval  20995  grporcan  21000  grpoinveu  21001  grpomndo  21125  r19.29d2r  23157  iundisjf  23227  xlt2addrd  23325  xrofsup  23327  iundisjfi  23356  rhmdvdsr  23422  neiptopuni  23443  neiptopnei  23445  tpr2rico  23466  cnextcn  23504  utoptop  23538  ucnima  23576  metust  23602  cfilucfil  23603  metustbl  23610  esumc  23712  esumfsup  23726  esumpcvgval  23734  hasheuni  23741  voliune  23849  volfiniune  23850  dya2icoseg2  23892  dya2iocnei  23896  dya2iocuni  23897  lgamucov2  24072  prodmolem2  24562  prodmo  24563  colinearex  25242  segcon2  25287  opnrebl2  25560  sdclem2  25776  heibor1lem  25856  2r19.29  26043  prtlem9  26055  prtlem11  26057  prter1  26070  prter2  26072  eldiophb  26159  rmxyelqirr  26318  hbtlem1  26650  hbtlem7  26652  stirlinglem13  27158  reuan  27281  2reu2rex  27284  usgra2edg1  27557  3v3e3cycl1  27768  1to3vfriendship  27841  2pthfrgrarn  27842  bnj31  28507  bnj1239  28600  bnj900  28723  bnj906  28724  bnj1398  28826  bnj1498  28853  hl2at  29663  cvrval4N  29672  athgt  29714  1dimN  29729  lhpexnle  30264  lhpexle1  30266  cdlemftr2  30824  cdlemftr1  30825  cdlemftr0  30826  cdlemg5  30863  cdlemg33c0  30960  mapdrvallem2  31904
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-ral 2624  df-rex 2625
  Copyright terms: Public domain W3C validator