Theorem exlimiv 1770

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

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

This inference, along with its many variants such as rexlimdv 2912, 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 1770 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 1798 and ax-8 1874. (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 1701	. 2 |- ( E. x ph -> E. x ps )
3		ax5e 1754	. 2 |- ( E. x ps -> ps )
4	2, 3	syl 17	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752

This theorem depends on definitions:  df-bi 188  df-ex 1658

This theorem is referenced by:  exlimivv  1771  equid  1844  equvin  1858  ax12v  1910  ax12vOLD  1911  19.8a  1912  19.8aOLD  1913  ax6e  2060  axc11n  2108  axc11nOLD  2109  sbcom2  2244  euex  2293  mo3  2306  mopick  2334  axext3  2403  gencl  3111  cgsexg  3114  gencbvex2  3126  vtocleg  3152  eqvinc  3198  elrabi  3225  sbcex2  3350  eluni  4222  intab  4286  uniintsn  4293  disjiun  4414  trint0  4535  bm1.3ii  4549  intex  4580  axpweq  4601  eunex  4617  eusvnf  4619  eusvnfb  4620  reusv2lem3  4627  unipw  4671  moabex  4680  nnullss  4683  exss  4684  mosubopt  4718  opelopabsb  4730  relop  5004  dmrnssfld  5112  dmsnopg  5326  unixp0  5389  iotauni  5577  iota1  5579  iota4  5583  dffv2  5954  fveqdmss  6032  eldmrexrnb  6044  exfo  6055  csbriota  6279  eusvobj2  6298  fnoprabg  6411  limuni3  6693  tfindsg  6701  findsg  6734  elxp5  6752  f1oexbi  6757  ffoss  6768  fo1stres  6831  fo2ndres  6832  eloprabi  6869  frxp  6917  suppimacnv  6936  mpt2xneldm  6969  mpt2xopxnop0  6972  reldmtpos  6992  dftpos4  7003  wfrlem2  7047  wfrlem3  7048  wfrlem4  7050  wfrdmcl  7055  wfrlem12  7058  tfrlem9  7114  ecdmn0  7417  mapprc  7487  ixpprc  7554  ixpn0  7565  bren  7589  brdomg  7590  ener  7626  en0  7642  en1  7646  en1b  7647  2dom  7652  fiprc  7661  pwdom  7733  domssex  7742  ssenen  7755  php  7765  isinf  7794  findcard2s  7821  hartogslem1  8066  brwdom  8091  brwdomn0  8093  wdompwdom  8102  unxpwdom2  8112  ixpiunwdom  8115  inf3  8149  infeq5  8151  omex  8157  epfrs  8223  rankwflemb  8272  bnd2  8372  oncard  8402  carduni  8423  pm54.43  8442  ween  8473  acnrcl  8480  acndom  8489  acndom2  8492  iunfictbso  8552  aceq3lem  8558  dfac4  8560  dfac5lem4  8564  dfac5lem5  8565  dfac5  8566  dfac2a  8567  dfac2  8568  dfacacn  8578  dfac12r  8583  kmlem2  8588  kmlem16  8602  ackbij2  8680  cff  8685  cardcf  8689  cfeq0  8693  cfsuc  8694  cff1  8695  cfcoflem  8709  coftr  8710  infpssr  8745  fin4en1  8746  isfin4-2  8751  enfin2i  8758  fin23lem21  8776  fin23lem30  8779  fin23lem41  8789  enfin1ai  8821  fin1a2lem7  8843  axcc2lem  8873  domtriomlem  8879  dcomex  8884  axdc2lem  8885  axdc3lem2  8888  axdc4lem  8892  axcclem  8894  ac6s  8921  zorn2lem7  8939  ttukey2g  8953  axdclem2  8957  axdc  8958  brdom3  8963  brdom5  8964  brdom4  8965  brdom7disj  8966  brdom6disj  8967  konigthlem  9000  pwcfsdom  9015  pwfseq  9096  tsk0  9195  gruina  9250  grothpw  9258  grothpwex  9259  grothomex  9261  grothac  9262  ltbtwnnq  9410  reclem2pr  9480  supsrlem  9542  supsr  9543  axpre-sup  9600  dedekindle  9805  nnunb  10872  ioorebas  11743  fzn0  11820  fzon0  11944  axdc4uzlem  12201  hasheqf1oi  12540  hash1snb  12597  hashf1lem2  12623  hashge2el2difr  12642  hashge3el3dif  12646  fi1uzind  12654  brfi1indALT  12657  swrdcl  12777  relexpindlem  13126  fclim  13616  climmo  13620  rlimdmo1  13680  cnso  14298  xpsfrnel2  15470  cicsym  15708  cictr  15709  brssc  15718  sscpwex  15719  initoid  15899  termoid  15900  initoeu1  15905  initoeu2lem1  15908  initoeu2  15910  termoeu1  15912  opifismgm  16500  grpidval  16502  subgint  16840  giclcl  16935  gicrcl  16936  gicsym  16937  gicen  16940  gicsubgen  16941  cntzssv  16981  giccyg  17533  brric2  17972  ricgic  17973  subrgint  18029  lmiclcl  18292  lmicrcl  18293  lmicsym  18294  abvn0b  18525  mpfrcl  18740  ply1frcl  18906  pf1rcl  18936  lmiclbs  19393  lmisfree  19398  lmictra  19401  mat1scmat  19562  neitr  20194  cmpsub  20413  bwth  20423  iuncon  20441  2ndcsb  20462  unisngl  20540  elpt  20585  ptclsg  20628  hmphsym  20795  hmphen  20798  haushmphlem  20800  cmphmph  20801  conhmph  20802  reghmph  20806  nrmhmph  20807  hmphdis  20809  indishmph  20811  hmphen2  20812  ufldom  20975  alexsubALTlem2  21061  alexsubALT  21064  metustfbas  21570  iunmbl2  22508  ioorcl2  22522  ioorinv2  22525  ioorinv2OLD  22530  opnmblALT  22559  plyssc  23152  aannenlem2  23283  aannenlem3  23284  mulog2sum  24373  istrkg2ld  24506  axcontlem4  24995  usgraedg4  25112  edgusgranbfin  25176  uvtx01vtx  25218  3v3e3cycl2  25390  wlknwwlknsur  25438  wlkiswwlksur  25445  wwlknndef  25463  wlk0  25487  clwwlknndef  25499  2spontn0vne  25613  rusgrasn  25671  eupath  25707  vdfrgra0  25748  usgn0fidegnn0  25755  frgrawopreglem2  25771  friendship  25848  shintcli  26980  strlem1  27901  eqvincg  28106  rexunirn  28125  ctex  28298  cnvoprab  28314  prsdm  28728  prsrn  28729  0elsiga  28944  sigaclcu  28947  issgon  28953  insiga  28967  omssubaddlem  29135  omssubadd  29136  omssubaddlemOLD  29139  omssubaddOLD  29140  bnj521  29553  bnj906  29749  bnj938  29756  bnj1018  29781  bnj1020  29782  bnj1125  29809  bnj1145  29810  mppspstlem  30217  frrlem2  30522  frrlem3  30523  frrlem4  30524  frrlem5e  30529  frrlem11  30533  txpss3v  30650  pprodss4v  30656  elsingles  30690  fnimage  30701  funpartlem  30714  funpartfun  30715  dfrdg4  30723  colinearex  30832  bj-axc11nv  31315  bj-eunex  31384  bj-mo3OLD  31417  bj-snglex  31535  mptsnunlem  31704  wl-sbcom2d  31855  wl-mo3t  31869  wl-ax12v2  31873  wl-19.8a  31874  ptrecube  31904  mblfinlem3  31943  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  indexdom  32025  prtlem16  32409  sbccomieg  35605  setindtr  35849  setindtrs  35850  dfac11  35890  lnmlmic  35916  gicabl  35927  isnumbasgrplem1  35930  rtrclex  36194  clcnvlem  36200  brtrclfv2  36289  snhesn  36352  frege55b  36463  frege55c  36484  iotain  36738  iotavalb  36751  sbiota1  36755  iunconlem2  37305  fnchoice  37323  stoweidlem59  37860  pfxcl  38797  funop  38882  funop1  38883  funsndifnop  38885  fundmge2nop  38889  nbgr1vtx  39190  edgusgrnbfin  39210  opmpt2ismgm  39426  nzerooringczr  39693