Theorem exlimiv 1641

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

This inference, along with our many variants such as rexlimdv 2789, 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

Step	Hyp	Ref	Expression
1		exlimiv.1	. . 3 |- ( ph -> ps )
2	1	eximi 1582	. 2 |- ( E. x ph -> E. x ps )
3		ax17e 1625	. 2 |- ( E. x ps -> ps )
4	2, 3	syl 16	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1547

This theorem is referenced by:  exlimivv  1642  19.8a  1758  a9e  1948  ax12olem1OLD  1977  ax10  1991  equvin  2051  ax11vALT  2146  mo  2276  mopick  2316  gencl  2944  cgsexg  2947  gencbvex2  2959  vtocleg  2982  eqvinc  3023  elrabi  3050  sbcex2  3170  eluni  3978  intab  4040  uniintsn  4047  disjiun  4162  trint0  4279  bm1.3ii  4293  intex  4316  axpweq  4336  eunex  4352  unipw  4374  moabex  4382  nnullss  4385  exss  4386  mosubopt  4414  opelopabsb  4425  eusvnf  4677  eusvnfb  4678  reusv2lem3  4685  limuni3  4791  tfindsg  4799  findsg  4831  relop  4982  dmrnssfld  5088  dmsnopg  5300  elxp5  5317  unixp0  5362  iotauni  5389  iota1  5391  iota4  5395  ffoss  5666  dffv2  5755  eldmrexrnb  5836  exfo  5846  fnoprabg  6130  fo1stres  6329  fo2ndres  6330  eloprabi  6372  frxp  6415  mpt2xopxnop0  6425  reldmtpos  6446  dftpos4  6457  eusvobj2  6541  tfrlem9  6605  ecdmn0  6906  mapprc  6981  ixpprc  7042  ixpn0  7053  bren  7076  brdomg  7077  ener  7113  en0  7129  en1  7133  en1b  7134  2dom  7138  fiprc  7147  pwdom  7218  domssex  7227  ssenen  7240  php  7250  isinf  7281  findcard2s  7308  hartogslem1  7467  brwdom  7491  brwdomn0  7493  wdompwdom  7502  unxpwdom2  7512  ixpiunwdom  7515  inf3  7546  infeq5  7548  omex  7554  epfrs  7623  rankwflemb  7675  bnd2  7773  oncard  7803  carduni  7824  pm54.43  7843  ween  7872  acnrcl  7879  acndom  7888  acndom2  7891  iunfictbso  7951  aceq3lem  7957  dfac4  7959  dfac5lem4  7963  dfac5lem5  7964  dfac5  7965  dfac2a  7966  dfac2  7967  dfacacn  7977  dfac12r  7982  kmlem2  7987  kmlem16  8001  ackbij2  8079  cff  8084  cardcf  8088  cfeq0  8092  cfsuc  8093  cff1  8094  cfcoflem  8108  coftr  8109  infpssr  8144  fin4en1  8145  isfin4-2  8150  enfin2i  8157  fin23lem21  8175  fin23lem30  8178  fin23lem41  8188  enfin1ai  8220  fin1a2lem7  8242  axcc2lem  8272  domtriomlem  8278  dcomex  8283  axdc2lem  8284  axdc3lem2  8287  axdc4lem  8291  axcclem  8293  ac6s  8320  zorn2lem7  8338  ttukey2g  8352  axdclem2  8356  axdc  8357  brdom3  8362  brdom5  8363  brdom4  8364  brdom7disj  8365  brdom6disj  8366  konigthlem  8399  pwcfsdom  8414  pwfseq  8495  tsk0  8594  gruina  8649  grothpw  8657  grothpwex  8658  grothomex  8660  grothac  8661  ltbtwnnq  8811  reclem2pr  8881  supsrlem  8942  supsr  8943  axpre-sup  9000  nnunb  10173  ioorebas  10962  fzn0  11026  fzon0  11111  axdc4uzlem  11276  hasheqf1oi  11590  hash1snb  11636  hashf1lem2  11660  brfi1uzind  11670  swrdcl  11721  fclim  12302  climmo  12306  rlimdmo1  12366  cnso  12801  xpsfrnel2  13745  brssc  13969  sscpwex  13970  grpidval  14662  subgint  14919  giclcl  15014  gicrcl  15015  gicsym  15016  gicen  15019  gicsubgen  15020  cntzssv  15082  giccyg  15464  subrgint  15845  lmiclcl  16097  lmicrcl  16098  lmicsym  16099  abvn0b  16317  neitr  17198  cmpsub  17417  iuncon  17444  2ndcsb  17465  elpt  17557  ptclsg  17600  hmphsym  17767  hmphen  17770  haushmphlem  17772  cmphmph  17773  conhmph  17774  reghmph  17778  nrmhmph  17779  hmphdis  17781  indishmph  17783  hmphen2  17784  ufldom  17947  alexsubALTlem2  18032  alexsubALT  18035  metustfbasOLD  18548  metustfbas  18549  iunmbl2  19404  ioorcl2  19417  ioorinv2  19420  opnmblALT  19448  mpfrcl  19892  pf1rcl  19922  plyssc  20072  aannenlem2  20199  aannenlem3  20200  mulog2sum  21184  usgraedg4  21359  edgusgranbfin  21412  uvtx01vtx  21454  3v3e3cycl2  21604  eupath  21656  shintcli  22784  strlem1  23706  eqvincg  23914  rexunirn  23931  ctex  24053  0elsiga  24450  sigaclcu  24453  issgon  24459  insiga  24473  relexpindlem  25092  dedekindle  25141  wfrlem2  25471  wfrlem3  25472  wfrlem4  25473  wfrlem9  25478  wfrlem12  25481  frrlem2  25496  frrlem3  25497  frrlem4  25498  frrlem5e  25503  frrlem11  25507  txpss3v  25632  pprodss4v  25638  elfix  25657  dffix2  25659  elsingles  25671  fnimage  25682  funpartlem  25695  funpartfun  25696  dfrdg4  25703  axcontlem4  25810  colinearex  25898  mblfinlem2  26144  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  indexdom  26326  prtlem16  26608  sbccomieg  26739  setindtr  26985  setindtrs  26986  dfac11  27028  lnmlmic  27054  gicabl  27131  isnumbasgrplem1  27134  lmiclbs  27175  lmisfree  27180  iotain  27485  iotavalb  27498  sbiota1  27502  fnchoice  27567  stoweidlem59  27675  2spontn0vne  28084  vdfrgra0  28126  vdgfrgra0  28127  frgrawopreglem2  28148  bnj521  28810  bnj906  29007  bnj938  29014  bnj1018  29039  bnj1020  29040  bnj1125  29067  bnj1145  29068  equvinNEW7  29233

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