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

Theorem exlimiv 1641
Description: Inference from Theorem 19.23 of [Margaris] p. 90.

This inference, along with our many variants such as rexlimdv 2793, is used to implement a metatheorem called "Rule C" that is given in many logic textbooks. See, for example, Rule C in [Mendelson] p. 81, Rule C in [Margaris] p. 40, or Rule C in Hirst and Hirst's A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.mathsci.appstate.edu/~hirstjl/primer/hirst.pdf.

In informal proofs, the statement "Let  C be an element such that..." almost always means an implicit application of Rule C.

In essence, Rule C states that if we can prove that some element  x exists satisfying a wff, i.e.  E. x ph ( x ) where  ph ( x ) has  x free, then we can use  ph ( C ) as a hypothesis for the proof where  C is a new (ficticious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier.

We cannot do this in Metamath directly. Instead, we use the original  ph (containing  x) as an antecedent for the main part of the proof. We eventually arrive at  ( ph  ->  ps ) where  ps is the theorem to be proved and does not contain  x. Then we apply exlimiv 1641 to arrive at  ( E. x ph  ->  ps ). Finally, we separately prove  E. x ph and detach it with modus ponens ax-mp 8 to arrive at the final theorem  ps. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 4-Dec-2017.)

Hypothesis
Ref Expression
exlimiv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
exlimiv  |-  ( E. x ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem exlimiv
StepHypRef Expression
1 exlimiv.1 . . 3  |-  ( ph  ->  ps )
21eximi 1582 . 2  |-  ( E. x ph  ->  E. x ps )
3 ax17e 1625 . 2  |-  ( E. x ps  ->  ps )
42, 3syl 16 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1547
This theorem is referenced by:  exlimivv  1642  19.8a  1758  a9e  1948  ax12olem1OLD  1977  ax10  1991  equvin  2055  ax11vALT  2150  mo  2280  mopick  2320  gencl  2948  cgsexg  2951  gencbvex2  2963  vtocleg  2986  eqvinc  3027  elrabi  3054  sbcex2  3174  eluni  3982  intab  4044  uniintsn  4051  disjiun  4166  trint0  4283  bm1.3ii  4297  intex  4320  axpweq  4340  eunex  4356  unipw  4378  moabex  4386  nnullss  4389  exss  4390  mosubopt  4418  opelopabsb  4429  eusvnf  4681  eusvnfb  4682  reusv2lem3  4689  limuni3  4795  tfindsg  4803  findsg  4835  relop  4986  dmrnssfld  5092  dmsnopg  5304  elxp5  5321  unixp0  5366  iotauni  5393  iota1  5395  iota4  5399  ffoss  5670  dffv2  5759  eldmrexrnb  5840  exfo  5850  fnoprabg  6134  fo1stres  6333  fo2ndres  6334  eloprabi  6376  frxp  6419  mpt2xopxnop0  6429  reldmtpos  6450  dftpos4  6461  eusvobj2  6545  tfrlem9  6609  ecdmn0  6910  mapprc  6985  ixpprc  7046  ixpn0  7057  bren  7080  brdomg  7081  ener  7117  en0  7133  en1  7137  en1b  7138  2dom  7142  fiprc  7151  pwdom  7222  domssex  7231  ssenen  7244  php  7254  isinf  7285  findcard2s  7312  hartogslem1  7471  brwdom  7495  brwdomn0  7497  wdompwdom  7506  unxpwdom2  7516  ixpiunwdom  7519  inf3  7550  infeq5  7552  omex  7558  epfrs  7627  rankwflemb  7679  bnd2  7777  oncard  7807  carduni  7828  pm54.43  7847  ween  7876  acnrcl  7883  acndom  7892  acndom2  7895  iunfictbso  7955  aceq3lem  7961  dfac4  7963  dfac5lem4  7967  dfac5lem5  7968  dfac5  7969  dfac2a  7970  dfac2  7971  dfacacn  7981  dfac12r  7986  kmlem2  7991  kmlem16  8005  ackbij2  8083  cff  8088  cardcf  8092  cfeq0  8096  cfsuc  8097  cff1  8098  cfcoflem  8112  coftr  8113  infpssr  8148  fin4en1  8149  isfin4-2  8154  enfin2i  8161  fin23lem21  8179  fin23lem30  8182  fin23lem41  8192  enfin1ai  8224  fin1a2lem7  8246  axcc2lem  8276  domtriomlem  8282  dcomex  8287  axdc2lem  8288  axdc3lem2  8291  axdc4lem  8295  axcclem  8297  ac6s  8324  zorn2lem7  8342  ttukey2g  8356  axdclem2  8360  axdc  8361  brdom3  8366  brdom5  8367  brdom4  8368  brdom7disj  8369  brdom6disj  8370  konigthlem  8403  pwcfsdom  8418  pwfseq  8499  tsk0  8598  gruina  8653  grothpw  8661  grothpwex  8662  grothomex  8664  grothac  8665  ltbtwnnq  8815  reclem2pr  8885  supsrlem  8946  supsr  8947  axpre-sup  9004  nnunb  10177  ioorebas  10966  fzn0  11030  fzon0  11115  axdc4uzlem  11280  hasheqf1oi  11594  hash1snb  11640  hashf1lem2  11664  brfi1uzind  11674  swrdcl  11725  fclim  12306  climmo  12310  rlimdmo1  12370  cnso  12805  xpsfrnel2  13749  brssc  13973  sscpwex  13974  grpidval  14666  subgint  14923  giclcl  15018  gicrcl  15019  gicsym  15020  gicen  15023  gicsubgen  15024  cntzssv  15086  giccyg  15468  subrgint  15849  lmiclcl  16101  lmicrcl  16102  lmicsym  16103  abvn0b  16321  neitr  17202  cmpsub  17421  iuncon  17448  2ndcsb  17469  elpt  17561  ptclsg  17604  hmphsym  17771  hmphen  17774  haushmphlem  17776  cmphmph  17777  conhmph  17778  reghmph  17782  nrmhmph  17783  hmphdis  17785  indishmph  17787  hmphen2  17788  ufldom  17951  alexsubALTlem2  18036  alexsubALT  18039  metustfbasOLD  18552  metustfbas  18553  iunmbl2  19408  ioorcl2  19421  ioorinv2  19424  opnmblALT  19452  mpfrcl  19896  pf1rcl  19926  plyssc  20076  aannenlem2  20203  aannenlem3  20204  mulog2sum  21188  usgraedg4  21363  edgusgranbfin  21416  uvtx01vtx  21458  3v3e3cycl2  21608  eupath  21660  shintcli  22788  strlem1  23710  eqvincg  23918  rexunirn  23935  ctex  24057  0elsiga  24454  sigaclcu  24457  issgon  24463  insiga  24477  relexpindlem  25096  dedekindle  25145  wfrlem2  25475  wfrlem3  25476  wfrlem4  25477  wfrlem9  25482  wfrlem12  25485  frrlem2  25500  frrlem3  25501  frrlem4  25502  frrlem5e  25507  frrlem11  25511  txpss3v  25636  pprodss4v  25642  elfix  25661  dffix2  25663  elsingles  25675  fnimage  25686  funpartlem  25699  funpartfun  25700  dfrdg4  25707  axcontlem4  25814  colinearex  25902  mblfinlem2  26148  ovoliunnfl  26151  voliunnfl  26153  volsupnfl  26154  indexdom  26330  prtlem16  26612  sbccomieg  26743  setindtr  26989  setindtrs  26990  dfac11  27032  lnmlmic  27058  gicabl  27135  isnumbasgrplem1  27138  lmiclbs  27179  lmisfree  27184  iotain  27489  iotavalb  27502  sbiota1  27506  fnchoice  27571  stoweidlem59  27679  2spontn0vne  28088  vdfrgra0  28130  vdgfrgra0  28131  frgrawopreglem2  28152  bnj521  28814  bnj906  29011  bnj938  29018  bnj1018  29043  bnj1020  29044  bnj1125  29071  bnj1145  29072  equvinNEW7  29237
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator