Theorem exlimiv 1932

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

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

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  exlimiiv  1933  exlimivv  1934  exsbim  2004  ax8  2120  ax9  2128  dfeumo  2536  mo3  2564  mo4  2566  moanimv  2619  euanv  2624  mopick  2625  clelab  2880  rexlimiva  3130  gencl  3471  cgsexg  3474  gencbvex2  3488  vtocleg  3498  eqvincg  3590  elrabi  3630  sbcex2  3789  sbccomlem  3807  eluni  4853  intab  4920  uniintsn  4927  dfiun2g  4972  disjiun  5073  trintss  5211  axrep6g  5225  sepexlem  5234  intex  5285  axpweq  5292  eunex  5332  eusvnf  5334  eusvnfb  5335  reusv2lem3  5342  axprglem  5378  axprg  5379  unipw  5402  moabex  5410  moabexOLD  5411  nnullss  5414  exss  5415  sbcop1  5441  mosubopt  5464  opelopabsb  5485  relop  5805  dmopab2rex  5872  dmrnssfld  5929  dmsnopg  6177  unixp0  6247  elsnxp  6255  iotauni2  6470  iotanul2  6471  iotaex  6474  iotauni  6475  iota1  6477  iota4  6479  dffv2  6935  fveqdmss  7030  eldmrexrnb  7044  exfo  7057  funop  7103  funopdmsn  7104  funsndifnop  7105  csbriota  7339  eusvobj2  7359  fnoprabg  7490  limuni3  7803  tfindsg  7812  findsg  7848  elxp5  7874  f1oexbi  7879  ffoss  7899  fo1stres  7968  fo2ndres  7969  eloprabi  8016  frxp  8076  suppimacnv  8124  mpoxneldm  8162  mpoxopxnop0  8165  reldmtpos  8184  dftpos4  8195  frrlem2  8237  frrlem3  8238  frrlem4  8239  frrlem8  8243  tfrlem9  8324  ecdmn0  8696  mapprc  8777  fsetprcnex  8809  ixpprc  8867  ixpn0  8878  bren  8903  brdomg  8905  domssl  8945  domssr  8946  ener  8948  en0  8965  en0ALT  8966  en0r  8967  en1  8971  en1b  8972  2dom  8977  fiprc  8991  dom0  9043  pwdom  9067  domssex  9076  ssenen  9089  dif1en  9096  findcard2s  9100  ensymfib  9118  php  9141  sdom1  9160  1sdom2dom  9164  isinf  9175  en1eqsn  9185  infn0  9212  pwfir  9227  fodomfir  9238  hartogslem1  9457  brwdom  9482  brwdomn0  9484  wdompwdom  9493  unxpwdom2  9503  ixpiunwdom  9505  elirrv  9512  infeq5  9558  brttrcl  9634  ttrcltr  9637  dmttrcl  9642  rnttrcl  9643  epfrs  9652  rankwflemb  9717  bnd2  9817  oncard  9884  carduni  9905  pm54.43  9925  ween  9957  acnrcl  9964  acndom  9973  acndom2  9976  iunfictbso  10036  aceq3lem  10042  dfac4  10044  dfac5lem4  10048  dfac5lem5  10049  dfac5lem4OLD  10050  dfac5  10051  dfac2a  10052  dfac2b  10053  dfacacn  10064  dfac12r  10069  kmlem2  10074  kmlem16  10088  ackbij2  10164  cff  10170  cardcf  10174  cfeq0  10178  cfsuc  10179  cff1  10180  cfcoflem  10194  coftr  10195  infpssr  10230  fin4en1  10231  isfin4-2  10236  enfin2i  10243  fin23lem21  10261  fin23lem30  10264  fin23lem41  10274  enfin1ai  10306  fin1a2lem7  10328  domtriomlem  10364  axdc2lem  10370  axdc3lem2  10373  axdc4lem  10377  axcclem  10379  ac6s  10406  zorn2lem7  10424  ttukey2g  10438  axdc  10443  brdom3  10450  brdom5  10451  brdom4  10452  brdom7disj  10453  brdom6disj  10454  konigthlem  10491  pwfseq  10587  tsk0  10686  gruina  10741  ltbtwnnq  10901  reclem2pr  10971  supsrlem  11034  supsr  11035  axpre-sup  11092  dedekindle  11310  nnunb  12433  ioorebas  13404  fzn0  13492  fzon0  13632  axdc4uzlem  13945  hasheqf1oi  14313  hash1snb  14381  hash1n0  14383  hashf1lem2  14418  hashle2pr  14439  hashge2el2difr  14443  hashge3el3dif  14449  fi1uzind  14469  brfi1indALT  14472  swrdcl  14608  pfxcl  14640  relexpindlem  15025  fclim  15515  climmo  15519  rlimdmo1  15580  cicsym  17771  cictr  17772  brssc  17781  sscpwex  17782  initoid  17968  termoid  17969  initoeu1  17978  initoeu2lem1  17981  initoeu2  17983  termoeu1  17985  opifismgm  18627  grpidval  18629  dfgrp3e  19016  subgint  19126  giclcl  19248  gicrcl  19249  gicsym  19250  gicen  19253  gicsubgen  19254  cntzssv  19303  symgvalstruct  19372  giccyg  19875  brric2  20483  ricgic  20484  subrngint  20537  subrgint  20572  abvn0b  20813  lmiclcl  21065  lmicrcl  21066  lmicsym  21067  nzerooringczr  21460  lmiclbs  21817  lmisfree  21822  lmictra  21825  mpfrcl  22063  ply1frcl  22283  pf1rcl  22314  mat1scmat  22504  toprntopon  22890  topnex  22961  neitr  23145  cmpsub  23365  bwth  23375  iunconn  23393  2ndcsb  23414  unisngl  23492  elpt  23537  ptclsg  23580  hmphsym  23747  hmphen  23750  haushmphlem  23752  cmphmph  23753  connhmph  23754  reghmph  23758  nrmhmph  23759  hmphdis  23761  indishmph  23763  hmphen2  23764  ufldom  23927  alexsubALTlem2  24013  alexsubALT  24016  metustfbas  24522  iunmbl2  25524  ioorcl2  25539  ioorinv2  25542  opnmblALT  25570  plyssc  26165  aannenlem2  26295  sltstr  27779  oncutlt  28256  istrkg2ld  28528  axcontlem4  29036  lfuhgr1v0e  29323  nbgr1vtx  29427  edgusgrnbfin  29442  cplgr1vlem  29498  cplgr1v  29499  fusgrn0degnn0  29568  g0wlk0  29719  wspthneq1eq2  29928  wlkswwlksf1o  29947  wwlksnndef  29973  wspthsnonn0vne  29985  eulerpath  30311  frgrwopreglem2  30383  friendship  30469  shintcli  31400  strlem1  32321  rexunirn  32561  iunrnmptss  32635  lsmsnorb  33451  mxidlnzrb  33540  prsdm  34058  prsrn  34059  0elsiga  34258  sigaclcu  34261  issgon  34267  insiga  34281  omssubaddlem  34443  omssubadd  34444  bnj906  35072  bnj938  35079  bnj1018g  35105  bnj1018  35106  bnj1020  35107  bnj1125  35134  bnj1145  35135  funen1cnv  35231  axprALT2  35253  fineqvac  35260  fineqvnttrclselem1  35265  fineqvnttrclselem2  35266  onvf1odlem4  35288  lfuhgr3  35302  loop1cycl  35319  satfrnmapom  35552  satf0op  35559  sat1el2xp  35561  dmopab3rexdif  35587  mppspstlem  35753  txpss3v  36058  pprodss4v  36064  elsingles  36098  fnimage  36109  funpartlem  36124  funpartfun  36125  dfrdg4  36133  colinearex  36242  dfttc4  36712  ttcexg  36714  regsfromregtco  36720  bj-cleljusti  36974  axc11n11r  36980  bj-exlimvmpi  37218  bj-snglex  37280  bj-unexg  37345  bj-bm1.3ii  37371  bj-axseprep  37381  bj-restpw  37404  mptsnunlem  37654  ctbssinf  37722  pibt2  37733  wl-ax12v2cl  37822  wl-moteq  37839  wl-sbcom2d  37886  wl-mo3t  37901  ptrecube  37941  mblfinlem3  37980  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  indexdom  38055  xrnss3v  38702  prtlem16  39315  ricsym  42964  riccrng1  42966  ricdrng1  42973  sbccomieg  43221  setindtr  43452  setindtrs  43453  dfac11  43490  lnmlmic  43516  gicabl  43527  isnumbasgrplem1  43529  iscard4  43960  rtrclex  44044  clcnvlem  44050  brtrclfv2  44154  snhesn  44213  frege55b  44324  frege55c  44345  grucollcld  44687  grumnudlem  44712  iotain  44844  iotavalb  44857  sbiota1  44861  iunconnlem2  45361  permaxun  45438  permac8prim  45441  fnchoice  45460  stoweidlem59  46487  vitali2  47122  nsssmfmbf  47207  fsetprcnexALT  47510  funop1  47731  sbcpr  47981  gricen  48401  grlicsym  48489  grlictr  48491  grlicen  48493  gricgrlic  48494  usgrexmpl12ngric  48514  usgrexmpl12ngrlic  48515  opmpoismgm  48643  mo0sn  49291  mofmo  49322  mofeu  49323  f1mo  49328  eloprab1st2nd  49343  neircl  49380  sectrcl  49497  invrcl  49499  isorcl  49508  isoval2  49510  initc  49566  uobffth  49693  uobeqw  49694  fullthinc  49925  termco  49956  termcbasmo  49958  isinito3  49975  oppctermhom  49979  functermc  49983  termc2  49993  eufunclem  49996  eufunc  49997  euendfunc  50001  arweuthinc  50004  arweutermc  50005  discsntermlem  50045  rellan  50098  relran  50099  termolmd  50145  setrec1lem3  50164  elsetrecs  50175  elpglem1  50186