Theorem exlimiv 1931

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

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

This inference, along with its many variants such as rexlimdv 3132, 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 3132. 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  2534  mo3  2561  mo4  2563  moanimv  2616  euanv  2621  mopick  2622  clelab  2877  rexlimiva  3126  gencl  3479  cgsexg  3482  gencbvex2  3497  vtocleg  3507  eqvincg  3599  elrabi  3639  sbcex2  3798  sbccomlem  3816  eluni  4863  intab  4930  uniintsn  4937  dfiun2g  4982  disjiun  5083  trintss  5220  axrep6g  5232  sepexlem  5241  intex  5286  axpweq  5293  eunex  5332  eusvnf  5334  eusvnfb  5335  reusv2lem3  5342  unipw  5395  moabex  5403  moabexOLD  5404  nnullss  5407  exss  5408  sbcop1  5433  mosubopt  5455  opelopabsb  5475  relop  5796  dmopab2rex  5863  dmrnssfld  5920  dmsnopg  6168  unixp0  6238  elsnxp  6246  iotauni2  6461  iotanul2  6462  iotaex  6465  iotauni  6466  iota1  6468  iota4  6470  dffv2  6926  fveqdmss  7020  eldmrexrnb  7034  exfo  7047  funop  7091  funopdmsn  7092  funsndifnop  7093  csbriota  7327  eusvobj2  7347  fnoprabg  7478  limuni3  7791  tfindsg  7800  findsg  7836  elxp5  7862  f1oexbi  7867  ffoss  7887  fo1stres  7956  fo2ndres  7957  eloprabi  8004  frxp  8065  suppimacnv  8113  mpoxneldm  8151  mpoxopxnop0  8154  reldmtpos  8173  dftpos4  8184  frrlem2  8226  frrlem3  8227  frrlem4  8228  frrlem8  8232  tfrlem9  8313  ecdmn0  8683  mapprc  8763  fsetprcnex  8795  ixpprc  8853  ixpn0  8864  bren  8889  brdomg  8891  domssl  8931  domssr  8932  ener  8934  en0  8951  en0ALT  8952  en0r  8953  en1  8957  en1b  8958  2dom  8963  fiprc  8977  dom0  9029  pwdom  9053  domssex  9062  ssenen  9075  dif1en  9082  findcard2s  9086  ensymfib  9104  php  9127  sdom1  9145  1sdom2dom  9149  isinf  9160  en1eqsn  9170  infn0  9197  pwfir  9212  fodomfir  9223  hartogslem1  9439  brwdom  9464  brwdomn0  9466  wdompwdom  9475  unxpwdom2  9485  ixpiunwdom  9487  elirrv  9494  infeq5  9538  brttrcl  9614  ttrcltr  9617  dmttrcl  9622  rnttrcl  9623  epfrs  9632  rankwflemb  9697  bnd2  9797  oncard  9864  carduni  9885  pm54.43  9905  ween  9937  acnrcl  9944  acndom  9953  acndom2  9956  iunfictbso  10016  aceq3lem  10022  dfac4  10024  dfac5lem4  10028  dfac5lem5  10029  dfac5lem4OLD  10030  dfac5  10031  dfac2a  10032  dfac2b  10033  dfacacn  10044  dfac12r  10049  kmlem2  10054  kmlem16  10068  ackbij2  10144  cff  10150  cardcf  10154  cfeq0  10158  cfsuc  10159  cff1  10160  cfcoflem  10174  coftr  10175  infpssr  10210  fin4en1  10211  isfin4-2  10216  enfin2i  10223  fin23lem21  10241  fin23lem30  10244  fin23lem41  10254  enfin1ai  10286  fin1a2lem7  10308  domtriomlem  10344  axdc2lem  10350  axdc3lem2  10353  axdc4lem  10357  axcclem  10359  ac6s  10386  zorn2lem7  10404  ttukey2g  10418  axdc  10423  brdom3  10430  brdom5  10431  brdom4  10432  brdom7disj  10433  brdom6disj  10434  konigthlem  10470  pwfseq  10566  tsk0  10665  gruina  10720  ltbtwnnq  10880  reclem2pr  10950  supsrlem  11013  supsr  11014  axpre-sup  11071  dedekindle  11288  nnunb  12388  ioorebas  13358  fzn0  13445  fzon0  13584  axdc4uzlem  13897  hasheqf1oi  14265  hash1snb  14333  hash1n0  14335  hashf1lem2  14370  hashle2pr  14391  hashge2el2difr  14395  hashge3el3dif  14401  fi1uzind  14421  brfi1indALT  14424  swrdcl  14560  pfxcl  14592  relexpindlem  14977  fclim  15467  climmo  15471  rlimdmo1  15532  cicsym  17719  cictr  17720  brssc  17729  sscpwex  17730  initoid  17916  termoid  17917  initoeu1  17926  initoeu2lem1  17929  initoeu2  17931  termoeu1  17933  opifismgm  18575  grpidval  18577  dfgrp3e  18961  subgint  19071  giclcl  19193  gicrcl  19194  gicsym  19195  gicen  19198  gicsubgen  19199  cntzssv  19248  symgvalstruct  19317  giccyg  19820  brric2  20430  ricgic  20431  subrngint  20484  subrgint  20519  abvn0b  20760  lmiclcl  21013  lmicrcl  21014  lmicsym  21015  nzerooringczr  21426  lmiclbs  21783  lmisfree  21788  lmictra  21791  mpfrcl  22031  ply1frcl  22253  pf1rcl  22284  mat1scmat  22474  toprntopon  22860  topnex  22931  neitr  23115  cmpsub  23335  bwth  23345  iunconn  23363  2ndcsb  23384  unisngl  23462  elpt  23507  ptclsg  23550  hmphsym  23717  hmphen  23720  haushmphlem  23722  cmphmph  23723  connhmph  23724  reghmph  23728  nrmhmph  23729  hmphdis  23731  indishmph  23733  hmphen2  23734  ufldom  23897  alexsubALTlem2  23983  alexsubALT  23986  metustfbas  24492  iunmbl2  25505  ioorcl2  25520  ioorinv2  25523  opnmblALT  25551  plyssc  26152  aannenlem2  26284  sslttr  27768  onscutlt  28221  istrkg2ld  28458  axcontlem4  28966  lfuhgr1v0e  29253  nbgr1vtx  29357  edgusgrnbfin  29372  cplgr1vlem  29428  cplgr1v  29429  fusgrn0degnn0  29499  g0wlk0  29650  wspthneq1eq2  29859  wlkswwlksf1o  29878  wwlksnndef  29904  wspthsnonn0vne  29916  eulerpath  30242  frgrwopreglem2  30314  friendship  30400  shintcli  31330  strlem1  32251  rexunirn  32492  iunrnmptss  32566  lsmsnorb  33400  mxidlnzrb  33489  prsdm  33999  prsrn  34000  0elsiga  34199  sigaclcu  34202  issgon  34208  insiga  34222  omssubaddlem  34384  omssubadd  34385  bnj906  35014  bnj938  35021  bnj1018g  35047  bnj1018  35048  bnj1020  35049  bnj1125  35076  bnj1145  35077  funen1cnv  35172  fineqvac  35211  fineqvnttrclselem1  35213  fineqvnttrclselem2  35214  onvf1odlem4  35222  lfuhgr3  35236  loop1cycl  35253  satfrnmapom  35486  satf0op  35493  sat1el2xp  35495  dmopab3rexdif  35521  mppspstlem  35687  txpss3v  35992  pprodss4v  35998  elsingles  36032  fnimage  36043  funpartlem  36058  funpartfun  36059  dfrdg4  36067  colinearex  36176  bj-cleljusti  36796  axc11n11r  36800  bj-exlimvmpi  37028  bj-snglex  37090  bj-unexg  37155  bj-bm1.3ii  37181  bj-restpw  37209  mptsnunlem  37455  ctbssinf  37523  pibt2  37534  wl-ax12v2cl  37623  wl-moteq  37631  wl-sbcom2d  37678  wl-mo3t  37693  ptrecube  37733  mblfinlem3  37772  ovoliunnfl  37775  voliunnfl  37777  volsupnfl  37778  indexdom  37847  xrnss3v  38478  prtlem16  39041  ricsym  42689  riccrng1  42691  ricdrng1  42698  sbccomieg  42950  setindtr  43181  setindtrs  43182  dfac11  43219  lnmlmic  43245  gicabl  43256  isnumbasgrplem1  43258  iscard4  43690  rtrclex  43774  clcnvlem  43780  brtrclfv2  43884  snhesn  43943  frege55b  44054  frege55c  44075  grucollcld  44417  grumnudlem  44442  iotain  44574  iotavalb  44587  sbiota1  44591  iunconnlem2  45091  permaxun  45168  permac8prim  45171  fnchoice  45190  stoweidlem59  46219  vitali2  46854  nsssmfmbf  46939  fsetprcnexALT  47224  funop1  47445  sbcpr  47683  gricen  48087  grlicsym  48175  grlictr  48177  grlicen  48179  gricgrlic  48180  usgrexmpl12ngric  48200  usgrexmpl12ngrlic  48201  opmpoismgm  48329  mo0sn  48977  mofmo  49008  mofeu  49009  f1mo  49014  eloprab1st2nd  49029  neircl  49066  sectrcl  49183  invrcl  49185  isorcl  49194  isoval2  49196  initc  49252  uobffth  49379  uobeqw  49380  fullthinc  49611  termco  49642  termcbasmo  49644  isinito3  49661  oppctermhom  49665  functermc  49669  termc2  49679  eufunclem  49682  eufunc  49683  euendfunc  49687  arweuthinc  49690  arweutermc  49691  discsntermlem  49731  rellan  49784  relran  49785  termolmd  49831  setrec1lem3  49850  elsetrecs  49861  elpglem1  49872