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

Theorem reximi 2650
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 2648 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  r19.40  2691  reu3  2955  2reu5  2973  ssiun  3944  iinss  3953  elunirnALT  5779  iiner  6731  erovlem  6754  xpf1o  7023  unbnn2  7114  scott0  7556  dfac2  7757  cflm  7876  alephsing  7902  numthcor  8121  zorng  8131  zornn0g  8132  ttukeyg  8144  uniimadom  8166  axgroth3  8453  qextlt  10530  qextle  10531  rexanre  11830  climi2  11985  climi0  11986  rlimres  12032  lo1res  12033  caurcvgr  12146  caurcvg2  12150  caucvgb  12152  vdwnnlem1  13042  efgrelexlemb  15059  eltg2b  16697  ordtbas2  16921  lmcvg  16992  cnprest  17017  lmcnp  17032  nrmsep2  17084  1stcfb  17171  islly2  17210  llycmpkgen  17247  txbas  17262  tx1stc  17344  tmdcn2  17772  metrest  18070  xrhmeo  18444  cmetcaulem  18714  iundisj  18905  limcresi  19235  elply2  19578  aalioulem2  19713  ulmf  19761  2sqlem7  20609  pntrsumbnd  20715  grpoidval  20883  grporcan  20888  grpoinveu  20889  grpomndo  21013  r19.29d2r  23181  xlt2addrd  23253  xrofsup  23255  tpr2rico  23296  iundisjfi  23363  iundisjf  23365  esumc  23430  esumpcvgval  23446  hasheuni  23453  colinearex  24683  segcon2  24728  fordisxex  24954  rspc2edv  24963  fldax5  25432  sallnei  25529  intopcoaconb  25540  altretop  25600  elhalop2  26069  isibg2a1  26119  isibg2a2  26120  isibg2a3  26121  opnrebl2  26236  sdclem2  26452  heibor1lem  26533  2r19.29  26720  prtlem9  26732  prtlem11  26734  prter1  26747  prter2  26749  eldiophb  26836  rmxyelqirr  26995  hbtlem1  27327  hbtlem7  27329  stirlinglem13  27835  reuan  27958  2reu2rex  27961  1to3vfriendship  28186  bnj31  28745  bnj1239  28838  bnj900  28961  bnj906  28962  bnj1398  29064  bnj1498  29091  hl2at  29594  cvrval4N  29603  athgt  29645  1dimN  29660  lhpexnle  30195  lhpexle1  30197  cdlemftr2  30755  cdlemftr1  30756  cdlemftr0  30757  cdlemg5  30794  cdlemg33c0  30891  mapdrvallem2  31835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator