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 3137, 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 3137. 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  2537  mo3  2565  mo4  2567  moanimv  2620  euanv  2625  mopick  2626  clelab  2881  rexlimiva  3131  gencl  3472  cgsexg  3475  gencbvex2  3489  vtocleg  3499  eqvincg  3591  elrabi  3631  sbcex2  3790  sbccomlem  3808  eluni  4854  intab  4921  uniintsn  4928  dfiun2g  4973  disjiun  5074  trintss  5211  axrep6g  5225  sepexlem  5234  intex  5281  axpweq  5288  eunex  5327  eusvnf  5329  eusvnfb  5330  reusv2lem3  5337  axprglem  5373  axprg  5374  unipw  5397  moabex  5405  moabexOLD  5406  nnullss  5409  exss  5410  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  7024  eldmrexrnb  7038  exfo  7051  funop  7096  funopdmsn  7097  funsndifnop  7098  csbriota  7332  eusvobj2  7352  fnoprabg  7483  limuni3  7796  tfindsg  7805  findsg  7841  elxp5  7867  f1oexbi  7872  ffoss  7892  fo1stres  7961  fo2ndres  7962  eloprabi  8009  frxp  8069  suppimacnv  8117  mpoxneldm  8155  mpoxopxnop0  8158  reldmtpos  8177  dftpos4  8188  frrlem2  8230  frrlem3  8231  frrlem4  8232  frrlem8  8236  tfrlem9  8317  ecdmn0  8689  mapprc  8770  fsetprcnex  8802  ixpprc  8860  ixpn0  8871  bren  8896  brdomg  8898  domssl  8938  domssr  8939  ener  8941  en0  8958  en0ALT  8959  en0r  8960  en1  8964  en1b  8965  2dom  8970  fiprc  8984  dom0  9036  pwdom  9060  domssex  9069  ssenen  9082  dif1en  9089  findcard2s  9093  ensymfib  9111  php  9134  sdom1  9153  1sdom2dom  9157  isinf  9168  en1eqsn  9178  infn0  9205  pwfir  9220  fodomfir  9231  hartogslem1  9450  brwdom  9475  brwdomn0  9477  wdompwdom  9486  unxpwdom2  9496  ixpiunwdom  9498  elirrv  9505  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  brric2  20474  ricgic  20475  subrngint  20528  subrgint  20563  abvn0b  20804  lmiclcl  21057  lmicrcl  21058  lmicsym  21059  nzerooringczr  21470  lmiclbs  21827  lmisfree  21832  lmictra  21835  mpfrcl  22073  ply1frcl  22293  pf1rcl  22324  mat1scmat  22514  toprntopon  22900  topnex  22971  neitr  23155  cmpsub  23375  bwth  23385  iunconn  23403  2ndcsb  23424  unisngl  23502  elpt  23547  ptclsg  23590  hmphsym  23757  hmphen  23760  haushmphlem  23762  cmphmph  23763  connhmph  23764  reghmph  23768  nrmhmph  23769  hmphdis  23771  indishmph  23773  hmphen2  23774  ufldom  23937  alexsubALTlem2  24023  alexsubALT  24026  metustfbas  24532  iunmbl2  25534  ioorcl2  25549  ioorinv2  25552  opnmblALT  25580  plyssc  26175  aannenlem2  26306  sltstr  27793  oncutlt  28270  istrkg2ld  28542  axcontlem4  29050  lfuhgr1v0e  29337  nbgr1vtx  29441  edgusgrnbfin  29456  cplgr1vlem  29512  cplgr1v  29513  fusgrn0degnn0  29583  g0wlk0  29734  wspthneq1eq2  29943  wlkswwlksf1o  29962  wwlksnndef  29988  wspthsnonn0vne  30000  eulerpath  30326  frgrwopreglem2  30398  friendship  30484  shintcli  31415  strlem1  32336  rexunirn  32576  iunrnmptss  32650  lsmsnorb  33466  mxidlnzrb  33555  prsdm  34074  prsrn  34075  0elsiga  34274  sigaclcu  34277  issgon  34283  insiga  34297  omssubaddlem  34459  omssubadd  34460  bnj906  35088  bnj938  35095  bnj1018g  35121  bnj1018  35122  bnj1020  35123  bnj1125  35150  bnj1145  35151  funen1cnv  35247  axprALT2  35269  fineqvac  35276  fineqvnttrclselem1  35281  fineqvnttrclselem2  35282  onvf1odlem4  35304  lfuhgr3  35318  loop1cycl  35335  satfrnmapom  35568  satf0op  35575  sat1el2xp  35577  dmopab3rexdif  35603  mppspstlem  35769  txpss3v  36074  pprodss4v  36080  elsingles  36114  fnimage  36125  funpartlem  36140  funpartfun  36141  dfrdg4  36149  colinearex  36258  dfttc4  36728  ttcexg  36730  regsfromregtco  36736  bj-cleljusti  36990  axc11n11r  36996  bj-exlimvmpi  37234  bj-snglex  37296  bj-unexg  37361  bj-bm1.3ii  37387  bj-axseprep  37397  bj-restpw  37420  mptsnunlem  37668  ctbssinf  37736  pibt2  37747  wl-ax12v2cl  37836  wl-moteq  37853  wl-sbcom2d  37900  wl-mo3t  37915  ptrecube  37955  mblfinlem3  37994  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  indexdom  38069  xrnss3v  38716  prtlem16  39329  ricsym  42978  riccrng1  42980  ricdrng1  42987  sbccomieg  43239  setindtr  43470  setindtrs  43471  dfac11  43508  lnmlmic  43534  gicabl  43545  isnumbasgrplem1  43547  iscard4  43978  rtrclex  44062  clcnvlem  44068  brtrclfv2  44172  snhesn  44231  frege55b  44342  frege55c  44363  grucollcld  44705  grumnudlem  44730  iotain  44862  iotavalb  44875  sbiota1  44879  iunconnlem2  45379  permaxun  45456  permac8prim  45459  fnchoice  45478  stoweidlem59  46505  vitali2  47140  nsssmfmbf  47225  fsetprcnexALT  47522  funop1  47743  sbcpr  47993  gricen  48413  grlicsym  48501  grlictr  48503  grlicen  48505  gricgrlic  48506  usgrexmpl12ngric  48526  usgrexmpl12ngrlic  48527  opmpoismgm  48655  mo0sn  49303  mofmo  49334  mofeu  49335  f1mo  49340  eloprab1st2nd  49355  neircl  49392  sectrcl  49509  invrcl  49511  isorcl  49520  isoval2  49522  initc  49578  uobffth  49705  uobeqw  49706  fullthinc  49937  termco  49968  termcbasmo  49970  isinito3  49987  oppctermhom  49991  functermc  49995  termc2  50005  eufunclem  50008  eufunc  50009  euendfunc  50013  arweuthinc  50016  arweutermc  50017  discsntermlem  50057  rellan  50110  relran  50111  termolmd  50157  setrec1lem3  50176  elsetrecs  50187  elpglem1  50198