Theorem exlimiv 1787

Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2004.

See exlimi 2006 for a more general version requiring more axioms.

This inference, along with its many variants such as rexlimdv 2889, 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.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 (fictitious) 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 1787 to arrive at ( E. x ph -> ps ). Finally, we separately prove E. x ph and detach it with modus ponens ax-mp 5 to arrive at the final theorem ps. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1816 and ax-8 1900. (Revised by Wolf Lammen, 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 1718	. 2 |- ( E. x ph -> E. x ps )
3		ax5e 1771	. 2 |- ( E. x ps -> ps )
4	2, 3	syl 17	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769

This theorem depends on definitions:  df-bi 190  df-ex 1675

This theorem is referenced by:  exlimiiv  1788  exlimivv  1789  equvin  1884  ax8  1904  ax9  1911  19.8aOLD  1947  sbcom2  2285  euex  2334  mo3  2347  mopick  2375  gencl  3089  cgsexg  3092  gencbvex2  3105  vtocleg  3132  eqvinc  3178  elrabi  3205  sbcex2  3330  eluni  4215  intab  4279  uniintsn  4286  disjiun  4407  trint0  4528  intex  4573  axpweq  4594  eunex  4610  eusvnf  4612  eusvnfb  4613  reusv2lem3  4620  unipw  4664  moabex  4673  nnullss  4676  exss  4677  mosubopt  4713  opelopabsb  4725  relop  5004  dmrnssfld  5112  dmsnopg  5326  unixp0  5389  iotauni  5577  iota1  5579  iota4  5583  dffv2  5961  fveqdmss  6040  eldmrexrnb  6052  exfo  6063  csbriota  6289  eusvobj2  6308  fnoprabg  6424  limuni3  6706  tfindsg  6714  findsg  6747  elxp5  6765  f1oexbi  6770  ffoss  6781  fo1stres  6844  fo2ndres  6845  eloprabi  6882  frxp  6933  suppimacnv  6952  mpt2xneldm  6985  mpt2xopxnop0  6988  reldmtpos  7007  dftpos4  7018  wfrlem2  7062  wfrlem3  7063  wfrlem4  7065  wfrdmcl  7070  wfrlem12  7073  tfrlem9  7129  ecdmn0  7432  mapprc  7502  ixpprc  7569  ixpn0  7580  bren  7604  brdomg  7605  ctex  7610  ener  7642  en0  7658  en1  7662  en1b  7663  2dom  7668  fiprc  7677  pwdom  7750  domssex  7759  ssenen  7772  php  7782  isinf  7811  findcard2s  7838  hartogslem1  8083  brwdom  8108  brwdomn0  8110  wdompwdom  8119  unxpwdom2  8129  ixpiunwdom  8132  infeq5  8168  omex  8174  epfrs  8241  rankwflemb  8290  bnd2  8390  oncard  8420  carduni  8441  pm54.43  8460  ween  8492  acnrcl  8499  acndom  8508  acndom2  8511  iunfictbso  8571  aceq3lem  8577  dfac4  8579  dfac5lem4  8583  dfac5lem5  8584  dfac5  8585  dfac2a  8586  dfac2  8587  dfacacn  8597  dfac12r  8602  kmlem2  8607  kmlem16  8621  ackbij2  8699  cff  8704  cardcf  8708  cfeq0  8712  cfsuc  8713  cff1  8714  cfcoflem  8728  coftr  8729  infpssr  8764  fin4en1  8765  isfin4-2  8770  enfin2i  8777  fin23lem21  8795  fin23lem30  8798  fin23lem41  8808  enfin1ai  8840  fin1a2lem7  8862  domtriomlem  8898  axdc2lem  8904  axdc3lem2  8907  axdc4lem  8911  axcclem  8913  ac6s  8940  zorn2lem7  8958  ttukey2g  8972  axdc  8977  brdom3  8982  brdom5  8983  brdom4  8984  brdom7disj  8985  brdom6disj  8986  konigthlem  9019  pwcfsdom  9034  pwfseq  9115  tsk0  9214  gruina  9269  grothpw  9277  ltbtwnnq  9429  reclem2pr  9499  supsrlem  9561  supsr  9562  axpre-sup  9619  dedekindle  9824  nnunb  10894  ioorebas  11765  fzn0  11842  fzon0  11968  axdc4uzlem  12227  hasheqf1oi  12566  hash1snb  12626  hashf1lem2  12652  hashge2el2difr  12671  hashge3el3dif  12675  fi1uzind  12683  brfi1indALT  12686  swrdcl  12812  relexpindlem  13175  fclim  13666  climmo  13670  rlimdmo1  13730  xpsfrnel2  15520  cicsym  15758  cictr  15759  brssc  15768  sscpwex  15769  initoid  15949  termoid  15950  initoeu1  15955  initoeu2lem1  15958  initoeu2  15960  termoeu1  15962  opifismgm  16550  grpidval  16552  subgint  16890  giclcl  16985  gicrcl  16986  gicsym  16987  gicen  16990  gicsubgen  16991  cntzssv  17031  giccyg  17583  brric2  18022  ricgic  18023  subrgint  18079  lmiclcl  18342  lmicrcl  18343  lmicsym  18344  abvn0b  18575  mpfrcl  18790  ply1frcl  18956  pf1rcl  18986  lmiclbs  19444  lmisfree  19449  lmictra  19452  mat1scmat  19613  neitr  20245  cmpsub  20464  bwth  20474  iuncon  20492  2ndcsb  20513  unisngl  20591  elpt  20636  ptclsg  20679  hmphsym  20846  hmphen  20849  haushmphlem  20851  cmphmph  20852  conhmph  20853  reghmph  20857  nrmhmph  20858  hmphdis  20860  indishmph  20862  hmphen2  20863  ufldom  21026  alexsubALTlem2  21112  alexsubALT  21115  metustfbas  21621  iunmbl2  22559  ioorcl2  22573  ioorinv2  22576  ioorinv2OLD  22581  opnmblALT  22610  plyssc  23203  aannenlem2  23334  mulog2sum  24424  istrkg2ld  24557  axcontlem4  25046  usgraedg4  25163  edgusgranbfin  25227  uvtx01vtx  25269  3v3e3cycl2  25441  wlknwwlknsur  25489  wlkiswwlksur  25496  wwlknndef  25514  wlk0  25538  clwwlknndef  25550  2spontn0vne  25664  rusgrasn  25722  eupath  25758  vdfrgra0  25799  usgn0fidegnn0  25806  frgrawopreglem2  25822  friendship  25899  shintcli  27031  strlem1  27952  eqvincg  28157  rexunirn  28176  cnvoprab  28357  prsdm  28769  prsrn  28770  0elsiga  28985  sigaclcu  28988  issgon  28994  insiga  29008  omssubaddlem  29176  omssubadd  29177  omssubaddlemOLD  29180  omssubaddOLD  29181  bnj521  29594  bnj906  29790  bnj938  29797  bnj1018  29822  bnj1020  29823  bnj1125  29850  bnj1145  29851  mppspstlem  30258  frrlem2  30564  frrlem3  30565  frrlem4  30566  frrlem5e  30571  frrlem11  30575  txpss3v  30694  pprodss4v  30700  elsingles  30734  fnimage  30745  funpartlem  30758  funpartfun  30759  dfrdg4  30767  colinearex  30876  bj-sbex  31284  bj-cleljusti  31323  bj-eunex  31459  bj-mo3OLD  31492  bj-snglex  31612  mptsnunlem  31785  wl-sbcom2d  31936  wl-mo3t  31950  wl-19.8a  31955  ptrecube  31985  mblfinlem3  32024  ovoliunnfl  32027  voliunnfl  32029  volsupnfl  32030  indexdom  32106  prtlem16  32486  sbccomieg  35681  setindtr  35924  setindtrs  35925  dfac11  35965  lnmlmic  35991  gicabl  36002  isnumbasgrplem1  36005  rtrclex  36269  clcnvlem  36275  brtrclfv2  36364  snhesn  36427  frege55b  36538  frege55c  36559  iotain  36812  iotavalb  36825  sbiota1  36829  iunconlem2  37372  fnchoice  37390  stoweidlem59  37958  pfxcl  38967  funop  39061  funop1  39062  funsndifnop  39064  fundmge2nop  39068  hash1n0  39115  nbgr1vtx  39476  edgusgrnbfin  39497  g01wlk0  39831  opmpt2ismgm  40080  nzerooringczr  40347