Theorem exlimiv 1931

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

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

This inference, along with its many variants such as rexlimdv 3135, 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 3135. 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 1931 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1932. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1968 and ax-8 2115. (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 1836	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
3		ax5e 1913	. 2 ⊢ (∃𝑥𝜓 → 𝜓)
4	2, 3	syl 17	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  exlimiiv  1932  exlimivv  1933  exsbim  2003  ax8  2119  ax9  2127  dfeumo  2536  mo3  2564  mo4  2566  moanimv  2619  euanv  2624  mopick  2625  clelab  2880  rexlimiva  3129  gencl  3482  cgsexg  3485  gencbvex2  3500  vtocleg  3510  eqvincg  3602  elrabi  3642  sbcex2  3801  sbccomlem  3819  eluni  4866  intab  4933  uniintsn  4940  dfiun2g  4985  disjiun  5086  trintss  5223  axrep6g  5235  sepexlem  5244  intex  5289  axpweq  5296  eunex  5335  eusvnf  5337  eusvnfb  5338  reusv2lem3  5345  unipw  5398  moabex  5406  moabexOLD  5407  nnullss  5410  exss  5411  sbcop1  5436  mosubopt  5458  opelopabsb  5478  relop  5799  dmopab2rex  5866  dmrnssfld  5923  dmsnopg  6171  unixp0  6241  elsnxp  6249  iotauni2  6464  iotanul2  6465  iotaex  6468  iotauni  6469  iota1  6471  iota4  6473  dffv2  6929  fveqdmss  7023  eldmrexrnb  7037  exfo  7050  funop  7094  funopdmsn  7095  funsndifnop  7096  csbriota  7330  eusvobj2  7350  fnoprabg  7481  limuni3  7794  tfindsg  7803  findsg  7839  elxp5  7865  f1oexbi  7870  ffoss  7890  fo1stres  7959  fo2ndres  7960  eloprabi  8007  frxp  8068  suppimacnv  8116  mpoxneldm  8154  mpoxopxnop0  8157  reldmtpos  8176  dftpos4  8187  frrlem2  8229  frrlem3  8230  frrlem4  8231  frrlem8  8235  tfrlem9  8316  ecdmn0  8687  mapprc  8767  fsetprcnex  8799  ixpprc  8857  ixpn0  8868  bren  8893  brdomg  8895  domssl  8935  domssr  8936  ener  8938  en0  8955  en0ALT  8956  en0r  8957  en1  8961  en1b  8962  2dom  8967  fiprc  8981  dom0  9033  pwdom  9057  domssex  9066  ssenen  9079  dif1en  9086  findcard2s  9090  ensymfib  9108  php  9131  sdom1  9150  1sdom2dom  9154  isinf  9165  en1eqsn  9175  infn0  9202  pwfir  9217  fodomfir  9228  hartogslem1  9447  brwdom  9472  brwdomn0  9474  wdompwdom  9483  unxpwdom2  9493  ixpiunwdom  9495  elirrv  9502  infeq5  9546  brttrcl  9622  ttrcltr  9625  dmttrcl  9630  rnttrcl  9631  epfrs  9640  rankwflemb  9705  bnd2  9805  oncard  9872  carduni  9893  pm54.43  9913  ween  9945  acnrcl  9952  acndom  9961  acndom2  9964  iunfictbso  10024  aceq3lem  10030  dfac4  10032  dfac5lem4  10036  dfac5lem5  10037  dfac5lem4OLD  10038  dfac5  10039  dfac2a  10040  dfac2b  10041  dfacacn  10052  dfac12r  10057  kmlem2  10062  kmlem16  10076  ackbij2  10152  cff  10158  cardcf  10162  cfeq0  10166  cfsuc  10167  cff1  10168  cfcoflem  10182  coftr  10183  infpssr  10218  fin4en1  10219  isfin4-2  10224  enfin2i  10231  fin23lem21  10249  fin23lem30  10252  fin23lem41  10262  enfin1ai  10294  fin1a2lem7  10316  domtriomlem  10352  axdc2lem  10358  axdc3lem2  10361  axdc4lem  10365  axcclem  10367  ac6s  10394  zorn2lem7  10412  ttukey2g  10426  axdc  10431  brdom3  10438  brdom5  10439  brdom4  10440  brdom7disj  10441  brdom6disj  10442  konigthlem  10479  pwfseq  10575  tsk0  10674  gruina  10729  ltbtwnnq  10889  reclem2pr  10959  supsrlem  11022  supsr  11023  axpre-sup  11080  dedekindle  11297  nnunb  12397  ioorebas  13367  fzn0  13454  fzon0  13593  axdc4uzlem  13906  hasheqf1oi  14274  hash1snb  14342  hash1n0  14344  hashf1lem2  14379  hashle2pr  14400  hashge2el2difr  14404  hashge3el3dif  14410  fi1uzind  14430  brfi1indALT  14433  swrdcl  14569  pfxcl  14601  relexpindlem  14986  fclim  15476  climmo  15480  rlimdmo1  15541  cicsym  17728  cictr  17729  brssc  17738  sscpwex  17739  initoid  17925  termoid  17926  initoeu1  17935  initoeu2lem1  17938  initoeu2  17940  termoeu1  17942  opifismgm  18584  grpidval  18586  dfgrp3e  18970  subgint  19080  giclcl  19202  gicrcl  19203  gicsym  19204  gicen  19207  gicsubgen  19208  cntzssv  19257  symgvalstruct  19326  giccyg  19829  brric2  20439  ricgic  20440  subrngint  20493  subrgint  20528  abvn0b  20769  lmiclcl  21022  lmicrcl  21023  lmicsym  21024  nzerooringczr  21435  lmiclbs  21792  lmisfree  21797  lmictra  21800  mpfrcl  22040  ply1frcl  22262  pf1rcl  22293  mat1scmat  22483  toprntopon  22869  topnex  22940  neitr  23124  cmpsub  23344  bwth  23354  iunconn  23372  2ndcsb  23393  unisngl  23471  elpt  23516  ptclsg  23559  hmphsym  23726  hmphen  23729  haushmphlem  23731  cmphmph  23732  connhmph  23733  reghmph  23737  nrmhmph  23738  hmphdis  23740  indishmph  23742  hmphen2  23743  ufldom  23906  alexsubALTlem2  23992  alexsubALT  23995  metustfbas  24501  iunmbl2  25514  ioorcl2  25529  ioorinv2  25532  opnmblALT  25560  plyssc  26161  aannenlem2  26293  sltstr  27783  oncutlt  28260  istrkg2ld  28532  axcontlem4  29040  lfuhgr1v0e  29327  nbgr1vtx  29431  edgusgrnbfin  29446  cplgr1vlem  29502  cplgr1v  29503  fusgrn0degnn0  29573  g0wlk0  29724  wspthneq1eq2  29933  wlkswwlksf1o  29952  wwlksnndef  29978  wspthsnonn0vne  29990  eulerpath  30316  frgrwopreglem2  30388  friendship  30474  shintcli  31404  strlem1  32325  rexunirn  32566  iunrnmptss  32640  lsmsnorb  33472  mxidlnzrb  33561  prsdm  34071  prsrn  34072  0elsiga  34271  sigaclcu  34274  issgon  34280  insiga  34294  omssubaddlem  34456  omssubadd  34457  bnj906  35086  bnj938  35093  bnj1018g  35119  bnj1018  35120  bnj1020  35121  bnj1125  35148  bnj1145  35149  funen1cnv  35244  fineqvac  35272  fineqvnttrclselem1  35277  fineqvnttrclselem2  35278  onvf1odlem4  35300  lfuhgr3  35314  loop1cycl  35331  satfrnmapom  35564  satf0op  35571  sat1el2xp  35573  dmopab3rexdif  35599  mppspstlem  35765  txpss3v  36070  pprodss4v  36076  elsingles  36110  fnimage  36121  funpartlem  36136  funpartfun  36137  dfrdg4  36145  colinearex  36254  regsfromregtr  36668  bj-cleljusti  36880  axc11n11r  36884  bj-exlimvmpi  37112  bj-snglex  37174  bj-unexg  37239  bj-bm1.3ii  37265  bj-restpw  37297  mptsnunlem  37543  ctbssinf  37611  pibt2  37622  wl-ax12v2cl  37711  wl-moteq  37719  wl-sbcom2d  37766  wl-mo3t  37781  ptrecube  37821  mblfinlem3  37860  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  indexdom  37935  xrnss3v  38566  prtlem16  39129  ricsym  42774  riccrng1  42776  ricdrng1  42783  sbccomieg  43035  setindtr  43266  setindtrs  43267  dfac11  43304  lnmlmic  43330  gicabl  43341  isnumbasgrplem1  43343  iscard4  43774  rtrclex  43858  clcnvlem  43864  brtrclfv2  43968  snhesn  44027  frege55b  44138  frege55c  44159  grucollcld  44501  grumnudlem  44526  iotain  44658  iotavalb  44671  sbiota1  44675  iunconnlem2  45175  permaxun  45252  permac8prim  45255  fnchoice  45274  stoweidlem59  46303  vitali2  46938  nsssmfmbf  47023  fsetprcnexALT  47308  funop1  47529  sbcpr  47767  gricen  48171  grlicsym  48259  grlictr  48261  grlicen  48263  gricgrlic  48264  usgrexmpl12ngric  48284  usgrexmpl12ngrlic  48285  opmpoismgm  48413  mo0sn  49061  mofmo  49092  mofeu  49093  f1mo  49098  eloprab1st2nd  49113  neircl  49150  sectrcl  49267  invrcl  49269  isorcl  49278  isoval2  49280  initc  49336  uobffth  49463  uobeqw  49464  fullthinc  49695  termco  49726  termcbasmo  49728  isinito3  49745  oppctermhom  49749  functermc  49753  termc2  49763  eufunclem  49766  eufunc  49767  euendfunc  49771  arweuthinc  49774  arweutermc  49775  discsntermlem  49815  rellan  49868  relran  49869  termolmd  49915  setrec1lem3  49934  elsetrecs  49945  elpglem1  49956