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

Theorem reximi 2866
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 2864 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1897   E.wrex 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-ral 2753  df-rex 2754
This theorem is referenced by:  r19.29d2r  2944  r19.40  2952  reu3  3239  2reu5  3259  ssiun  4333  iinss  4342  elsnxp  5396  elunirn  6180  iiner  7460  erovlem  7484  xpf1o  7759  unbnn2  7853  scott0  8382  dfac2  8586  cflm  8705  alephsing  8731  numthcor  8949  zorng  8959  zornn0g  8960  ttukeyg  8972  uniimadom  8994  axgroth3  9281  qextlt  11524  qextle  11525  mptnn0fsuppd  12241  hash2sspr  12676  cshword  12929  rexanre  13457  climi2  13623  climi0  13624  rlimres  13670  lo1res  13671  caurcvgr  13786  caurcvgrOLD  13787  caurcvg2  13792  caucvgb  13794  prodmolem2  14037  prodmo  14038  vdwnnlem1  14993  cshwsiun  15118  isnmnd  16588  efgrelexlemb  17448  nn0gsumfz0  17662  pmatcollpw2lem  19849  eltg2b  20022  neiptopuni  20194  neiptopnei  20196  ordtbas2  20255  lmcvg  20326  cnprest  20353  lmcnp  20368  nrmsep2  20420  bwth  20473  1stcfb  20508  islly2  20547  llycmpkgen  20615  txbas  20630  tx1stc  20713  cnextcn  21130  tmdcn2  21152  utoptop  21297  ucnima  21344  cfiluweak  21358  metrest  21587  metust  21621  cfilucfil  21622  metustbl  21629  xrhmeo  22022  cmetcaulem  22306  iundisj  22549  limcresi  22888  elply2  23198  aalioulem2  23337  ulmf  23385  lgamucov2  24012  2sqlem7  24346  pntrsumbnd  24452  istrkg2ld  24556  tgisline  24720  usgra2edg1  25158  3v3e3cycl1  25420  wwlkn0  25465  1to3vfriendship  25784  2pthfrgrarn  25785  grpoidval  25992  grporcan  25997  grpoinveu  25998  grpomndo  26122  iundisjf  28247  xlt2addrd  28386  xrge0infssOLD  28389  xrofsup  28401  iundisjfi  28420  rhmdvdsr  28629  tpr2rico  28766  esumc  28920  esumfsup  28939  esumpcvgval  28947  hasheuni  28954  esumiun  28963  voliune  29100  volfiniune  29101  dya2icoseg2  29148  dya2iocnei  29152  dya2iocuni  29153  omssubaddlem  29175  omssubadd  29176  omssubaddlemOLD  29179  omssubaddOLD  29180  afsval  29536  bnj31  29573  bnj1239  29665  bnj900  29788  bnj906  29789  bnj1398  29891  bnj1498  29918  colinearex  30875  segcon2  30920  opnrebl2  31025  sdclem2  32115  heibor1lem  32185  2r19.29  32472  prtlem9  32480  prtlem11  32482  prter1  32495  prter2  32497  hl2at  33014  cvrval4N  33023  athgt  33065  1dimN  33080  lhpexnle  33615  lhpexle1  33617  cdlemftr2  34177  cdlemftr1  34178  cdlemftr0  34179  cdlemg5  34216  cdlemg33c0  34313  mapdrvallem2  35257  eldiophb  35643  rmxyelqirr  35802  hbtlem1  36026  hbtlem7  36028  ss2iundf  36295  founiiun  37483  founiiun0  37502  stirlinglem13  37985  fourierdlem112  38119  reuan  38638  2reu2rex  38641  gboagbo  38894  cshword2  39017  umgr3v3e3cycl  39924  usg2edgneu  39996
  Copyright terms: Public domain W3C validator