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

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

This inference, along with our many variants such as rexlimdv 2679, 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 1624 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 1566 . 2  |-  ( E. x ph  ->  E. x ps )
3 ax17e 1608 . 2  |-  ( E. x ps  ->  ps )
42, 3syl 15 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531
This theorem is referenced by:  exlimivv  1625  ax12olem1  1880  equvin  1954  mo  2178  mopick  2218  gencl  2829  cgsexg  2832  gencbvex2  2844  vtocleg  2867  eqvinc  2908  sbcex2  3053  eluni  3846  intab  3908  uniintsn  3915  disjiun  4029  trint0  4146  bm1.3ii  4160  intex  4183  axpweq  4203  eunex  4219  unipw  4240  moabex  4248  nnullss  4251  exss  4252  mosubopt  4280  opelopabsb  4291  eusvnf  4545  eusvnfb  4546  reusv2lem3  4553  limuni3  4659  tfindsg  4667  findsg  4699  relop  4850  dmrnssfld  4954  dmsnopg  5160  elxp5  5177  unixp0  5222  iotauni  5247  iota1  5249  iota4  5253  ffoss  5521  dffv2  5608  exfo  5694  fnoprabg  5961  fo1stres  6159  fo2ndres  6160  eloprabi  6202  frxp  6241  reldmtpos  6258  dftpos4  6269  eusvobj2  6353  tfrlem9  6417  ecdmn0  6718  mapprc  6792  ixpprc  6853  ixpn0  6864  bren  6887  brdomg  6888  ener  6924  en0  6940  en1  6944  en1b  6945  2dom  6949  fiprc  6958  pwdom  7029  domssex  7038  ssenen  7051  php  7061  isinf  7092  findcard2s  7115  hartogslem1  7273  brwdom  7297  brwdomn0  7299  wdompwdom  7308  unxpwdom2  7318  ixpiunwdom  7321  inf3  7352  infeq5  7354  omex  7360  epfrs  7429  rankwflemb  7481  bnd2  7579  oncard  7609  carduni  7630  pm54.43  7649  ween  7678  acnrcl  7685  acndom  7694  acndom2  7697  iunfictbso  7757  aceq3lem  7763  dfac4  7765  dfac5lem4  7769  dfac5lem5  7770  dfac5  7771  dfac2a  7772  dfac2  7773  dfacacn  7783  dfac12r  7788  kmlem2  7793  kmlem16  7807  ackbij2  7885  cff  7890  cardcf  7894  cfeq0  7898  cfsuc  7899  cff1  7900  cfcoflem  7914  coftr  7915  infpssr  7950  fin4en1  7951  isfin4-2  7956  enfin2i  7963  fin23lem21  7981  fin23lem30  7984  fin23lem41  7994  enfin1ai  8026  fin1a2lem7  8048  axcc2lem  8078  domtriomlem  8084  dcomex  8089  axdc2lem  8090  axdc3lem2  8093  axdc4lem  8097  axcclem  8099  ac6s  8127  zorn2lem7  8145  ttukey2g  8159  axdclem2  8163  axdc  8164  brdom3  8169  brdom5  8170  brdom4  8171  brdom7disj  8172  brdom6disj  8173  konigthlem  8206  pwcfsdom  8221  pwfseq  8302  tsk0  8401  gruina  8456  grothpw  8464  grothpwex  8465  grothomex  8467  grothac  8468  ltbtwnnq  8618  reclem2pr  8688  supsrlem  8749  supsr  8750  axpre-sup  8807  nnunb  9977  ioorebas  10761  fzn0  10825  fzon0  10907  axdc4uzlem  11060  hashf1lem2  11410  swrdcl  11468  fclim  12043  climmo  12047  rlimdmo1  12107  cnso  12541  xpsfrnel2  13483  brssc  13707  sscpwex  13708  grpidval  14400  subgint  14657  giclcl  14752  gicrcl  14753  gicsym  14754  gicen  14757  gicsubgen  14758  cntzssv  14820  giccyg  15202  subrgint  15583  lmiclcl  15839  lmicrcl  15840  lmicsym  15841  abvn0b  16059  cmpsub  17143  iuncon  17170  2ndcsb  17191  elpt  17283  ptclsg  17325  hmphsym  17489  hmphen  17492  haushmphlem  17494  cmphmph  17495  conhmph  17496  reghmph  17500  nrmhmph  17501  hmphdis  17503  indishmph  17505  hmphen2  17506  ufldom  17673  alexsubALTlem2  17758  alexsubALT  17761  iunmbl2  18930  ioorcl2  18943  ioorinv2  18946  opnmblALT  18974  mpfrcl  19418  pf1rcl  19448  plyssc  19598  aannenlem2  19725  aannenlem3  19726  mulog2sum  20702  shintcli  21924  strlem1  22846  eqvincg  23146  rexunirn  23156  ctex  23351  0elsiga  23490  sigaclcu  23493  issgon  23499  insiga  23513  eupath  23920  relexpindlem  24051  dedekindle  24098  wfrlem2  24328  wfrlem3  24329  wfrlem4  24330  wfrlem9  24335  wfrlem12  24338  frrlem2  24353  frrlem3  24354  frrlem4  24355  frrlem5e  24360  frrlem11  24364  txpss3v  24489  pprodss4v  24495  elfix  24514  dffix2  24516  elsingles  24528  fnimage  24539  funpartlem  24552  funpartfun  24553  dfrdg4  24560  axcontlem4  24667  colinearex  24755  ovoliunnfl  25001  copsexgb  25069  prj1b  25182  prj3  25183  prl  25270  inposet  25381  osneisi  25634  dmhmph  25636  rnhmph  25637  fisub  25657  limptlimpr2lem1  25677  bwt2  25695  indexdom  26516  prtlem16  26840  sbccomieg  26973  setindtr  27220  setindtrs  27221  dfac11  27263  lnmlmic  27289  gicabl  27366  isnumbasgrplem1  27369  lmiclbs  27410  lmisfree  27415  iotain  27720  iotavalb  27733  sbiota1  27737  fnchoice  27803  stoweidlem53  27905  mpt2xopxnop0  28197  uvtx01vtx  28305  3v3e3cycl2  28410  bnj521  29081  bnj906  29278  bnj938  29285  bnj1018  29310  bnj1020  29311  bnj1125  29338  bnj1145  29339  equvinNEW7  29504
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator