Theorem exlimiv 1949

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

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

This inference, along with its many variants such as rexlimdv 3160, 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 3160. In informal proofs, the statement "Let 𝐶 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 𝑥 exists satisfying a wff, i.e. ∃𝑥𝜑(𝑥) where 𝜑(𝑥) has 𝑥 free, then we can use 𝜑(𝐶) as a hypothesis for the proof where 𝐶 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 𝜑 (containing 𝑥) as an antecedent for the main part of the proof. We eventually arrive at (𝜑 → 𝜓) where 𝜓 is the theorem to be proved and does not contain 𝑥. Then we apply exlimiv 1949 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1950. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1986 and ax-8 2143. (Revised by Wolf Lammen, 4-Dec-2017.)

Hypothesis

Ref	Expression
exlimiv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
exlimiv	⊢ (∃𝑥𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem exlimiv

Step	Hyp	Ref	Expression
1		exlimiv.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	eximi 1854	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
3		ax5e 1931	. 2 ⊢ (∃𝑥𝜓 → 𝜓)
4	2, 3	syl 17	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  exlimiiv  1950  exlimivv  1951  exsbim  2021  ax8  2147  ax9  2155  dfeumo  2562  mo3  2590  mo4  2592  moanimv  2645  euanv  2650  mopick  2651  clelab  2905  rexlimiva  3154  gencl  3494  cgsexg  3497  gencbvex2  3510  vtocleg  3520  eqvincg  3606  elrabi  3645  sbcex2  3802  sbccomlem  3820  eluni  4865  intab  4933  uniintsn  4940  dfiun2g  4984  disjiun  5085  trintss  5223  axrep6g  5237  sepexlem  5246  intex  5297  axpweq  5304  eunex  5344  eusvnf  5346  eusvnfb  5347  reusv2lem3  5354  axprglem  5390  axprg  5391  unipw  5414  moabex  5422  moabexOLD  5423  nnullss  5426  exss  5427  sbcop1  5453  mosubopt  5476  opelopabsb  5497  relop  5818  dmopab2rex  5889  dmrnssfld  5946  dmsnopg  6195  unixp0  6265  elsnxp  6273  iotauni2  6488  iotanul2  6489  iotaex  6492  iotauni  6493  iota1  6495  iota4  6497  dffv2  6957  fveqdmss  7054  eldmrexrnb  7068  exfo  7081  funop  7127  funopdmsn  7128  funsndifnop  7129  csbriota  7363  eusvobj2  7383  fnoprabg  7514  limuni3  7827  tfindsg  7836  findsg  7873  elxp5  7899  f1oexbi  7904  ffoss  7922  fo1stres  7991  fo2ndres  7992  eloprabi  8039  frxp  8100  suppimacnv  8148  mpoxneldm  8186  mpoxopxnop0  8189  reldmtpos  8208  dftpos4  8219  frrlem2  8262  frrlem3  8263  frrlem4  8264  frrlem8  8268  tfrlem9  8350  ecdmn0  8725  mapprc  8806  fsetprcnex  8837  ixpprc  8895  ixpn0  8906  bren  8931  brdomg  8933  domssl  8973  domssr  8974  ener  8976  en0  8993  en0ALT  8994  en0r  8995  en1  8999  en1b  9000  2dom  9005  fiprc  9019  dom0  9071  pwdom  9095  domssex  9104  ssenen  9117  dif1en  9124  findcard2s  9128  ensymfib  9146  php  9169  sdom1  9188  1sdom2dom  9192  isinf  9203  en1eqsn  9213  infn0  9240  pwfir  9255  fodomfir  9266  hartogslem1  9484  brwdom  9509  brwdomn0  9511  wdompwdom  9520  unxpwdom2  9530  ixpiunwdom  9532  elirrvOLD  9540  infeq5  9586  brttrcl  9662  ttrcltr  9665  dmttrcl  9670  rnttrcl  9671  epfrs  9680  rankwflemb  9745  bnd2  9845  oncard  9912  carduni  9933  pm54.43  9953  ween  9985  acnrcl  9992  acndom  10001  acndom2  10004  iunfictbso  10064  aceq3lem  10070  dfac4  10072  dfac5lem4  10076  dfac5lem5  10077  dfac5lem4OLD  10078  dfac5  10079  dfac2a  10080  dfac2b  10081  dfacacn  10092  dfac12r  10097  kmlem2  10102  kmlem16  10116  ackbij2  10192  cff  10198  cardcf  10202  cfeq0  10207  cfsuc  10208  cff1  10209  cfcoflem  10223  coftr  10224  infpssr  10259  fin4en1  10260  isfin4-2  10265  enfin2i  10272  fin23lem21  10290  fin23lem30  10293  fin23lem41  10303  enfin1ai  10335  fin1a2lem7  10357  domtriomlem  10393  axdc2lem  10399  axdc3lem2  10402  axdc4lem  10406  axcclem  10408  ac6s  10435  zorn2lem7  10453  ttukey2g  10467  axdc  10472  brdom3  10479  brdom5  10480  brdom4  10481  brdom7disj  10482  brdom6disj  10483  konigthlem  10520  pwfseq  10616  tsk0  10715  gruina  10770  ltbtwnnq  10930  reclem2pr  11000  supsrlem  11063  supsr  11064  axpre-sup  11121  dedekindle  11341  nnunb  12471  ioorebas  13449  fzn0  13537  fzon0  13677  axdc4uzlem  13990  hasheqf1oi  14358  hash1snb  14426  hash1n0  14428  hashf1lem2  14463  hashle2pr  14484  hashge2el2difr  14488  hashge3el3dif  14494  fi1uzind  14514  brfi1indALT  14517  swrdcl  14653  pfxcl  14685  relexpindlem  15070  fclim  15571  climmo  15575  rlimdmo1  15636  cicsym  17828  cictr  17829  brssc  17838  sscpwex  17839  initoid  18025  termoid  18026  initoeu1  18035  initoeu2lem1  18038  initoeu2  18040  termoeu1  18042  opifismgm  18684  grpidval  18686  dfgrp3e  19073  subgint  19183  giclcl  19304  gicrcl  19305  gicsym  19306  gicen  19309  gicsubgen  19310  cntzssv  19359  symgvalstruct  19428  giccyg  19931  ricsym  20542  brric2  20543  ricgic  20544  subrngint  20597  subrgint  20632  abvn0b  20873  lmiclcl  21125  lmicrcl  21126  lmicsym  21127  nzerooringczr  21520  lmiclbs  21877  lmisfree  21882  lmictra  21885  mpfrcl  22126  ply1frcl  22369  pf1rcl  22400  mat1scmat  22587  toprntopon  22973  topnex  23044  neitr  23228  cmpsub  23448  bwth  23458  iunconn  23476  2ndcsb  23497  unisngl  23575  elpt  23620  ptclsg  23663  hmphsym  23830  hmphen  23833  haushmphlem  23835  cmphmph  23836  connhmph  23837  reghmph  23841  nrmhmph  23842  hmphdis  23844  indishmph  23846  hmphen2  23847  ufldom  24010  alexsubALTlem2  24096  alexsubALT  24099  metustfbas  24605  iunmbl2  25607  ioorcl2  25622  ioorinv2  25625  opnmblALT  25653  plyssc  26248  aannenlem2  26381  sltstr  27868  oncutlt  28345  istrkg2ld  28617  axcontlem4  29125  lfuhgr1v0e  29412  nbgr1vtx  29516  edgusgrnbfin  29531  cplgr1vlem  29587  cplgr1v  29588  fusgrn0degnn0  29657  g0wlk0  29808  wspthneq1eq2  30017  wlkswwlksf1o  30036  wwlksnndef  30062  wspthsnonn0vne  30074  eulerpath  30400  frgrwopreglem2  30472  friendship  30558  shintcli  31489  strlem1  32410  rexunirn  32650  iunrnmptss  32725  lsmsnorb  33538  mxidlnzrb  33629  prsdm  34172  prsrn  34173  0elsiga  34372  sigaclcu  34375  issgon  34381  insiga  34395  omssubaddlem  34557  omssubadd  34558  bnj906  35186  bnj938  35193  bnj1018g  35219  bnj1018  35220  bnj1020  35221  bnj1125  35248  bnj1145  35249  funen1cnv  35343  axprALT2  35366  fineqvac  35373  fineqvnttrclselem1  35378  fineqvnttrclselem2  35379  onvf1odlem4  35410  vonf1oonfo  35419  lfuhgr3  35431  loop1cycl  35448  satfrnmapom  35681  satf0op  35688  sat1el2xp  35690  dmopab3rexdif  35716  mppspstlem  35882  txpss3v  36187  pprodss4v  36193  elsingles  36227  fnimage  36238  funpartlem  36253  funpartfun  36254  dfrdg4  36262  colinearex  36371  dfttc4  36851  ttcexg  36853  regsfromregtco  36859  bj-cleljusti  37113  axc11n11r  37119  bj-exlimvmpi  37357  bj-snglex  37419  bj-unexg  37484  bj-bm1.3ii  37510  bj-axseprep  37520  bj-restpw  37543  mptsnunlem  37793  ctbssinf  37861  pibt2  37872  wl-ax12v2cl  37961  wl-moteq  37978  wl-sbcom2d  38025  wl-mo3t  38040  ptrecube  38080  mblfinlem3  38119  ovoliunnfl  38122  voliunnfl  38124  volsupnfl  38125  indexdom  38194  xrnss3v  38841  prtlem16  39454  riccrng1  43100  ricdrng1  43107  sbccomieg  43331  setindtr  43562  setindtrs  43563  dfac11  43600  lnmlmic  43626  gicabl  43637  isnumbasgrplem1  43639  iscard4  44070  rtrclex  44154  clcnvlem  44160  brtrclfv2  44264  snhesn  44323  frege55b  44434  frege55c  44455  grucollcld  44797  grumnudlem  44822  iotain  44954  iotavalb  44967  sbiota1  44971  iunconnlem2  45471  permaxun  45548  permac8prim  45551  fnchoice  45570  stoweidlem59  46594  vitali2  47229  nsssmfmbf  47314  fsetprcnexALT  47617  funop1  47838  sbcpr  48088  gricen  48508  grlicsym  48596  grlictr  48598  grlicen  48600  gricgrlic  48601  usgrexmpl12ngric  48621  usgrexmpl12ngrlic  48622  opmpoismgm  48750  mo0sn  49398  mofmo  49429  mofeu  49430  f1mo  49435  eloprab1st2nd  49450  neircl  49487  sectrcl  49604  invrcl  49606  isorcl  49615  isoval2  49617  initc  49673  uobffth  49800  uobeqw  49801  fullthinc  50032  termco  50063  termcbasmo  50065  isinito3  50082  oppctermhom  50086  functermc  50090  termc2  50100  eufunclem  50103  eufunc  50104  euendfunc  50108  arweuthinc  50111  arweutermc  50112  discsntermlem  50152  rellan  50205  relran  50206  termolmd  50252  setrec1lem3  50271  elsetrecs  50282  elpglem1  50293