Theorem exlimiv 1937

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

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

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

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  exlimiiv  1938  exlimivv  1939  exsbim  2009  ax8  2125  ax9  2133  dfeumo  2540  mo3  2568  mo4  2570  moanimv  2623  euanv  2628  mopick  2629  clelab  2883  rexlimiva  3132  gencl  3472  cgsexg  3475  gencbvex2  3489  vtocleg  3499  eqvincg  3586  elrabi  3625  sbcex2  3783  sbccomlem  3801  eluni  4841  intab  4908  uniintsn  4915  dfiun2g  4959  disjiun  5060  trintss  5198  axrep6g  5212  sepexlem  5221  intex  5272  axpweq  5279  eunex  5319  eusvnf  5321  eusvnfb  5322  reusv2lem3  5329  axprglem  5365  axprg  5366  unipw  5389  moabex  5397  moabexOLD  5398  nnullss  5401  exss  5402  sbcop1  5428  mosubopt  5451  opelopabsb  5472  relop  5792  dmopab2rex  5859  dmrnssfld  5916  dmsnopg  6164  unixp0  6234  elsnxp  6242  iotauni2  6457  iotanul2  6458  iotaex  6461  iotauni  6462  iota1  6464  iota4  6466  dffv2  6922  fveqdmss  7019  eldmrexrnb  7033  exfo  7046  funop  7092  funopdmsn  7093  funsndifnop  7094  csbriota  7328  eusvobj2  7348  fnoprabg  7479  limuni3  7792  tfindsg  7801  findsg  7837  elxp5  7863  f1oexbi  7868  ffoss  7888  fo1stres  7957  fo2ndres  7958  eloprabi  8005  frxp  8066  suppimacnv  8114  mpoxneldm  8152  mpoxopxnop0  8155  reldmtpos  8174  dftpos4  8185  frrlem2  8227  frrlem3  8228  frrlem4  8229  frrlem8  8233  tfrlem9  8314  ecdmn0  8686  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  elirrvOLD  9503  infeq5  9549  brttrcl  9625  ttrcltr  9628  dmttrcl  9633  rnttrcl  9634  epfrs  9643  rankwflemb  9708  bnd2  9808  oncard  9875  carduni  9896  pm54.43  9916  ween  9948  acnrcl  9955  acndom  9964  acndom2  9967  iunfictbso  10027  aceq3lem  10033  dfac4  10035  dfac5lem4  10039  dfac5lem5  10040  dfac5lem4OLD  10041  dfac5  10042  dfac2a  10043  dfac2b  10044  dfacacn  10055  dfac12r  10060  kmlem2  10065  kmlem16  10079  ackbij2  10155  cff  10161  cardcf  10165  cfeq0  10169  cfsuc  10170  cff1  10171  cfcoflem  10185  coftr  10186  infpssr  10221  fin4en1  10222  isfin4-2  10227  enfin2i  10234  fin23lem21  10252  fin23lem30  10255  fin23lem41  10265  enfin1ai  10297  fin1a2lem7  10319  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  axdc4lem  10368  axcclem  10370  ac6s  10397  zorn2lem7  10415  ttukey2g  10429  axdc  10434  brdom3  10441  brdom5  10442  brdom4  10443  brdom7disj  10444  brdom6disj  10445  konigthlem  10482  pwfseq  10578  tsk0  10677  gruina  10732  ltbtwnnq  10892  reclem2pr  10962  supsrlem  11025  supsr  11026  axpre-sup  11083  dedekindle  11301  nnunb  12424  ioorebas  13395  fzn0  13483  fzon0  13623  axdc4uzlem  13936  hasheqf1oi  14304  hash1snb  14372  hash1n0  14374  hashf1lem2  14409  hashle2pr  14430  hashge2el2difr  14434  hashge3el3dif  14440  fi1uzind  14460  brfi1indALT  14463  swrdcl  14599  pfxcl  14631  relexpindlem  15016  fclim  15506  climmo  15510  rlimdmo1  15571  cicsym  17762  cictr  17763  brssc  17772  sscpwex  17773  initoid  17959  termoid  17960  initoeu1  17969  initoeu2lem1  17972  initoeu2  17974  termoeu1  17976  opifismgm  18618  grpidval  18620  dfgrp3e  19007  subgint  19117  giclcl  19239  gicrcl  19240  gicsym  19241  gicen  19244  gicsubgen  19245  cntzssv  19294  symgvalstruct  19363  giccyg  19866  ricsym  20477  brric2  20478  ricgic  20479  subrngint  20532  subrgint  20567  abvn0b  20808  lmiclcl  21060  lmicrcl  21061  lmicsym  21062  nzerooringczr  21455  lmiclbs  21812  lmisfree  21817  lmictra  21820  mpfrcl  22061  ply1frcl  22304  pf1rcl  22335  mat1scmat  22522  toprntopon  22908  topnex  22979  neitr  23163  cmpsub  23383  bwth  23393  iunconn  23411  2ndcsb  23432  unisngl  23510  elpt  23555  ptclsg  23598  hmphsym  23765  hmphen  23768  haushmphlem  23770  cmphmph  23771  connhmph  23772  reghmph  23776  nrmhmph  23777  hmphdis  23779  indishmph  23781  hmphen2  23782  ufldom  23945  alexsubALTlem2  24031  alexsubALT  24034  metustfbas  24540  iunmbl2  25542  ioorcl2  25557  ioorinv2  25560  opnmblALT  25588  plyssc  26183  aannenlem2  26313  sltstr  27797  oncutlt  28274  istrkg2ld  28546  axcontlem4  29054  lfuhgr1v0e  29341  nbgr1vtx  29445  edgusgrnbfin  29460  cplgr1vlem  29516  cplgr1v  29517  fusgrn0degnn0  29586  g0wlk0  29737  wspthneq1eq2  29946  wlkswwlksf1o  29965  wwlksnndef  29991  wspthsnonn0vne  30003  eulerpath  30329  frgrwopreglem2  30401  friendship  30487  shintcli  31418  strlem1  32339  rexunirn  32579  iunrnmptss  32654  lsmsnorb  33474  mxidlnzrb  33563  prsdm  34098  prsrn  34099  0elsiga  34298  sigaclcu  34301  issgon  34307  insiga  34321  omssubaddlem  34483  omssubadd  34484  bnj906  35112  bnj938  35119  bnj1018g  35145  bnj1018  35146  bnj1020  35147  bnj1125  35174  bnj1145  35175  funen1cnv  35269  axprALT2  35290  fineqvac  35297  fineqvnttrclselem1  35302  fineqvnttrclselem2  35303  onvf1odlem4  35334  lfuhgr3  35348  loop1cycl  35365  satfrnmapom  35598  satf0op  35605  sat1el2xp  35607  dmopab3rexdif  35633  mppspstlem  35799  txpss3v  36104  pprodss4v  36110  elsingles  36144  fnimage  36155  funpartlem  36170  funpartfun  36171  dfrdg4  36179  colinearex  36288  dfttc4  36758  ttcexg  36760  regsfromregtco  36766  bj-cleljusti  37020  axc11n11r  37026  bj-exlimvmpi  37264  bj-snglex  37326  bj-unexg  37391  bj-bm1.3ii  37417  bj-axseprep  37427  bj-restpw  37450  mptsnunlem  37700  ctbssinf  37768  pibt2  37779  wl-ax12v2cl  37868  wl-moteq  37885  wl-sbcom2d  37932  wl-mo3t  37947  ptrecube  37987  mblfinlem3  38026  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  indexdom  38101  xrnss3v  38748  prtlem16  39361  riccrng1  43007  ricdrng1  43014  sbccomieg  43238  setindtr  43469  setindtrs  43470  dfac11  43507  lnmlmic  43533  gicabl  43544  isnumbasgrplem1  43546  iscard4  43977  rtrclex  44061  clcnvlem  44067  brtrclfv2  44171  snhesn  44230  frege55b  44341  frege55c  44362  grucollcld  44704  grumnudlem  44729  iotain  44861  iotavalb  44874  sbiota1  44878  iunconnlem2  45378  permaxun  45455  permac8prim  45458  fnchoice  45477  stoweidlem59  46502  vitali2  47137  nsssmfmbf  47222  fsetprcnexALT  47525  funop1  47746  sbcpr  47996  gricen  48416  grlicsym  48504  grlictr  48506  grlicen  48508  gricgrlic  48509  usgrexmpl12ngric  48529  usgrexmpl12ngrlic  48530  opmpoismgm  48658  mo0sn  49306  mofmo  49337  mofeu  49338  f1mo  49343  eloprab1st2nd  49358  neircl  49395  sectrcl  49512  invrcl  49514  isorcl  49523  isoval2  49525  initc  49581  uobffth  49708  uobeqw  49709  fullthinc  49940  termco  49971  termcbasmo  49973  isinito3  49990  oppctermhom  49994  functermc  49998  termc2  50008  eufunclem  50011  eufunc  50012  euendfunc  50016  arweuthinc  50019  arweutermc  50020  discsntermlem  50060  rellan  50113  relran  50114  termolmd  50160  setrec1lem3  50179  elsetrecs  50190  elpglem1  50201