Theorem exlimiv 1709

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

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

This inference, along with its many variants such as rexlimdv 2933, 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 1709 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 1734 and ax-8 1806. (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 1643	. 2 |- ( E. x ph -> E. x ps )
3		ax5e 1693	. 2 |- ( E. x ps -> ps )
4	2, 3	syl 16	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691

This theorem depends on definitions:  df-bi 185  df-ex 1600

This theorem is referenced by:  exlimivv  1710  equvin  1790  ax12v  1841  ax12vOLD  1842  19.8a  1843  19.8aOLD  1844  ax6e  1988  axc11n  2035  axc11nOLD  2036  equvinOLD  2076  sbcom2  2175  euex  2294  mo3  2309  mo3OLD  2310  mopick  2342  mopickOLD  2343  axext3  2423  gencl  3125  cgsexg  3128  gencbvex2  3140  vtocleg  3166  eqvinc  3212  elrabi  3240  sbcex2  3367  eluni  4237  intab  4302  uniintsn  4309  disjiun  4427  trint0  4547  bm1.3ii  4561  intex  4593  axpweq  4614  eunex  4630  eusvnf  4632  eusvnfb  4633  reusv2lem3  4640  unipw  4687  moabex  4696  nnullss  4699  exss  4700  mosubopt  4735  opelopabsb  4747  relop  5143  dmrnssfld  5251  dmsnopg  5469  unixp0  5531  iotauni  5553  iota1  5555  iota4  5559  dffv2  5931  fveqdmss  6011  eldmrexrnb  6023  exfo  6034  csbriota  6254  eusvobj2  6274  fnoprabg  6388  limuni3  6672  tfindsg  6680  findsg  6712  elxp5  6730  f1oexbi  6735  ffoss  6746  fo1stres  6809  fo2ndres  6810  eloprabi  6847  frxp  6895  suppimacnv  6914  mpt2xopxnop0  6945  reldmtpos  6965  dftpos4  6976  tfrlem9  7056  ecdmn0  7356  mapprc  7426  ixpprc  7492  ixpn0  7503  bren  7527  brdomg  7528  ener  7564  en0  7580  en1  7584  en1b  7585  2dom  7590  fiprc  7599  pwdom  7671  domssex  7680  ssenen  7693  php  7703  isinf  7735  findcard2s  7763  hartogslem1  7970  brwdom  7996  brwdomn0  7998  wdompwdom  8007  unxpwdom2  8017  ixpiunwdom  8020  inf3  8055  infeq5  8057  omex  8063  epfrs  8165  rankwflemb  8214  bnd2  8314  oncard  8344  carduni  8365  pm54.43  8384  ween  8419  acnrcl  8426  acndom  8435  acndom2  8438  iunfictbso  8498  aceq3lem  8504  dfac4  8506  dfac5lem4  8510  dfac5lem5  8511  dfac5  8512  dfac2a  8513  dfac2  8514  dfacacn  8524  dfac12r  8529  kmlem2  8534  kmlem16  8548  ackbij2  8626  cff  8631  cardcf  8635  cfeq0  8639  cfsuc  8640  cff1  8641  cfcoflem  8655  coftr  8656  infpssr  8691  fin4en1  8692  isfin4-2  8697  enfin2i  8704  fin23lem21  8722  fin23lem30  8725  fin23lem41  8735  enfin1ai  8767  fin1a2lem7  8789  axcc2lem  8819  domtriomlem  8825  dcomex  8830  axdc2lem  8831  axdc3lem2  8834  axdc4lem  8838  axcclem  8840  ac6s  8867  zorn2lem7  8885  ttukey2g  8899  axdclem2  8903  axdc  8904  brdom3  8909  brdom5  8910  brdom4  8911  brdom7disj  8912  brdom6disj  8913  konigthlem  8946  pwcfsdom  8961  pwfseq  9045  tsk0  9144  gruina  9199  grothpw  9207  grothpwex  9208  grothomex  9210  grothac  9211  ltbtwnnq  9359  reclem2pr  9429  supsrlem  9491  supsr  9492  axpre-sup  9549  dedekindle  9748  nnunb  10797  ioorebas  11635  fzn0  11709  fzon0  11824  axdc4uzlem  12071  hasheqf1oi  12403  hash1snb  12458  hashf1lem2  12484  hashge3el3dif  12503  brfi1uzind  12511  swrdcl  12625  fclim  13355  climmo  13359  rlimdmo1  13419  cnso  13857  xpsfrnel2  14839  brssc  15060  sscpwex  15061  opifismgm  15759  grpidval  15761  subgint  16099  giclcl  16194  gicrcl  16195  gicsym  16196  gicen  16199  gicsubgen  16200  cntzssv  16240  giccyg  16776  brric2  17268  ricgic  17269  subrgint  17325  lmiclcl  17590  lmicrcl  17591  lmicsym  17592  abvn0b  17825  mpfrcl  18061  ply1frcl  18229  pf1rcl  18259  lmiclbs  18745  lmisfree  18750  lmictra  18753  mat1scmat  18914  neitr  19554  cmpsub  19773  bwth  19783  bwthOLD  19784  iuncon  19802  2ndcsb  19823  unisngl  19901  elpt  19946  ptclsg  19989  hmphsym  20156  hmphen  20159  haushmphlem  20161  cmphmph  20162  conhmph  20163  reghmph  20167  nrmhmph  20168  hmphdis  20170  indishmph  20172  hmphen2  20173  ufldom  20336  alexsubALTlem2  20421  alexsubALT  20424  metustfbasOLD  20941  metustfbas  20942  iunmbl2  21840  ioorcl2  21854  ioorinv2  21857  opnmblALT  21885  plyssc  22470  aannenlem2  22597  aannenlem3  22598  mulog2sum  23594  istrkg2ld  23730  axcontlem4  24142  usgraedg4  24259  edgusgranbfin  24322  uvtx01vtx  24364  3v3e3cycl2  24536  wlknwwlknsur  24584  wlkiswwlksur  24591  wwlknndef  24609  wlk0  24633  clwwlknndef  24645  2spontn0vne  24759  rusgrasn  24817  eupath  24853  vdfrgra0  24894  usgn0fidegnn0  24901  frgrawopreglem2  24917  friendship  24994  shintcli  26119  strlem1  27041  eqvincg  27246  rexunirn  27262  ctex  27403  cnvoprab  27418  prsdm  27769  prsrn  27770  0elsiga  27987  sigaclcu  27990  issgon  27996  insiga  28010  mppspstlem  28804  relexpindlem  28935  wfrlem2  29319  wfrlem3  29320  wfrlem4  29321  wfrlem9  29326  wfrlem12  29329  frrlem2  29363  frrlem3  29364  frrlem4  29365  frrlem5e  29370  frrlem11  29374  txpss3v  29503  pprodss4v  29509  elsingles  29543  fnimage  29554  funpartlem  29567  funpartfun  29568  dfrdg4  29575  colinearex  29685  wl-sbcom2d  29986  wl-mo3t  29996  mblfinlem3  30028  ovoliunnfl  30031  voliunnfl  30033  volsupnfl  30034  indexdom  30200  prtlem16  30585  sbccomieg  30701  setindtr  30941  setindtrs  30942  dfac11  30983  lnmlmic  31009  gicabl  31022  isnumbasgrplem1  31025  iotain  31278  iotavalb  31291  sbiota1  31295  fnchoice  31358  stoweidlem59  31730  opmpt2ismgm  32332  iunconlem2  33468  bnj521  33525  bnj906  33721  bnj938  33728  bnj1018  33753  bnj1020  33754  bnj1125  33781  bnj1145  33782  bj-equsexvv  34061  bj-axc11nv  34064  bj-eunex  34133  bj-snglex  34279  snhesn  37496  frege55b  37592  frege55c  37614