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

Theorem eximi 1602
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eximi.1
Assertion
Ref Expression
eximi

Proof of Theorem eximi
StepHypRef Expression
1 exim 1601 . 2
2 eximi.1 . 2
31, 2mpg 1572 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  E.wex 1565
This theorem is referenced by:  2eximi  1603  eximii  1604  exsimpl  1619  exsimpr  1620  19.29r2  1626  19.29x  1627  19.40-2  1638  exlimiv  1662  speimfw  1673  sbimi  1683  19.12  1872  19.12OLD  1873  equs4OLD  2005  axc9lem3  2012  exdistrf  2074  exdistrfOLD  2075  equs45f  2096  sbequiOLD  2124  eumo0  2338  eupickbOLD  2397  2eu2ex  2407  reximi2  2866  cgsexg  3046  gencbvex  3057  vtocl3  3067  eqvinc  3125  axrep2  4431  bm1.3ii  4442  ax6vsep  4443  axnul  4446  dminss  5273  imainss  5274  iotaex  5418  fv3  5720  ssimaex  5772  dffv2  5780  exfo  5877  oprabid  6127  zfrep6  6552  frxp  6688  tz7.48-1  6862  enssdom  7296  fineqvlem  7488  infcntss  7546  infeq5  7759  omex  7765  rankuni  7956  scott0  7979  acni3  8099  acnnum  8104  dfac3  8173  dfac9  8187  kmlem1  8201  cflm  8301  cfcof  8325  axdc4lem  8506  axcclem  8508  ac6c4  8532  ac6s  8535  ac6s2  8537  axdclem2  8571  brdom3  8577  brdom5  8578  brdom4  8579  axpowndlem2  8644  nqpr  9062  ltexprlem4  9087  reclem2pr  9096  drsdirfi  14949  2ndcsb  18527  fbssint  18885  isfil2  18903  alexsubALTlem3  19095  lpbl  19548  metustfbasOLD  19610  metustfbas  19611  3v3e3cycl2  22672  ex-natded9.26-2  22749  eqvincg  24986  19.9d2rf  24990  rexunirn  25003  ceqsexv2d  25010  cnvoprab  25153  fmcncfil  25540  0elsiga  25737  ddemeas  25832  fundmpss  26729  exisym1  27513  heiborlem3  27894  spsbce-2  28807  iotaexeu  28846  iotasbc  28847  fnchoice  28926  rfcnnnub  28933  stoweidlem35  29009  stoweidlem57  29031  hash1to3  29416  relopabVD  30483  a6e2ndeqVD  30491  2uasbanhVD  30493  a6e2ndeqALT  30513  bnj168  30567  bnj593  30583  bnj607  30757  bnj600  30760  bnj916  30774  bj-sels  30946  bj-snsetex  30947  bj-snglss  30953  bj-snglex  30956  19.12vAUX11  31006  exdistrfNEW11  31057  equs4NEW11  31085  sbequiNEW11  31131  equs45fNEW11  31172  19.12OLD11  31237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581
This theorem depends on definitions:  df-bi 179  df-ex 1566
  Copyright terms: Public domain W3C validator