Theorem exlimiv 1963

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

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

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  exlimiiv  1964  exlimivv  1965  exsbim  2035  ax8  2151  ax9  2159  dfeumo  2561  mo3  2589  mo4  2591  moanimv  2644  euanv  2649  mopick  2650  clelab  2904  rexlimiva  3155  gencl  3491  cgsexg  3494  gencbvex2  3507  vtocleg  3516  eqvincg  3602  elrabi  3641  sbcex2  3799  sbccomlem  3817  eluni  4870  intab  4938  uniintsn  4945  dfiun2g  4988  disjiun  5091  trintss  5231  axrep6g  5245  sepexlem  5256  intex  5308  axpweq  5315  eunex  5355  eusvnf  5357  eusvnfb  5358  reusv2lem3  5365  axprglem  5401  axprg  5402  unipw  5425  moabex  5433  moabexOLD  5434  nnullss  5437  exss  5438  sbcop1  5464  mosubopt  5487  opelopabsb  5508  relop  5830  dmopab2rex  5901  dmrnssfld  5958  dmsnopg  6209  unixp0  6281  elsnxp  6289  iotauni2  6505  iotanul2  6506  iotaex  6509  iotauni  6510  iota1  6512  iota4  6514  dffv2  6973  fveqdmss  7071  eldmrexrnb  7085  exfo  7098  funop  7146  funopdmsn  7147  funsndifnop  7148  csbriota  7385  eusvobj2  7405  fnoprabg  7536  limuni3  7848  tfindsg  7857  findsg  7894  elxp5  7920  f1oexbi  7925  ffoss  7943  fo1stres  8012  fo2ndres  8013  eloprabi  8060  frxp  8124  suppimacnv  8172  mpoxneldm  8210  mpoxopxnop0  8213  reldmtpos  8232  dftpos4  8243  frrlem2  8286  frrlem3  8287  frrlem4  8288  frrlem8  8292  tfrlem9  8374  ecdmn0  8749  mapprc  8830  fsetprcnex  8863  ixpprc  8926  ixpn0  8937  bren  8962  brdomg  8964  domssl  9004  domssr  9005  ener  9007  en0  9024  en0ALT  9025  en0r  9026  en1  9030  en1b  9031  funen1cnv  9035  2dom  9037  fiprc  9051  dom0  9103  pwdom  9127  domssex  9136  ssenen  9149  dif1en  9156  findcard2s  9160  ensymfib  9178  php  9201  sdom1  9220  1sdom2dom  9224  isinf  9235  en1eqsn  9245  infn0  9272  pwfir  9286  fodomfir  9297  hartogslem1  9514  brwdom  9539  brwdomn0  9541  wdompwdom  9550  unxpwdom2  9560  ixpiunwdom  9562  elirrvOLD  9570  infeq5  9616  brttrcl  9692  ttrcltr  9695  dmttrcl  9700  rnttrcl  9701  epfrs  9710  rankwflemb  9775  scottex  9872  bnd2  9895  oncard  9965  carduni  9986  pm54.43  10006  ween  10038  acnrcl  10045  acndom  10054  acndom2  10057  iunfictbso  10117  aceq3lem  10123  dfac4  10125  dfac5lem4  10129  dfac5lem5  10130  dfac5  10131  dfac2a  10132  dfac2b  10133  dfacacn  10144  dfac12r  10149  kmlem2  10154  kmlem16  10168  ackbij2  10244  cff  10249  cardcf  10253  cfeq0  10258  cfsuc  10259  cff1  10260  cfcoflem  10274  coftr  10275  infpssr  10310  fin4en1  10311  isfin4-2  10316  enfin2i  10323  fin23lem21  10341  fin23lem30  10344  fin23lem41  10354  enfin1ai  10386  fin1a2lem7  10408  domtriomlem  10444  axdc2lem  10450  axdc3lem2  10453  axdc4lem  10457  axcclem  10459  ac6s  10486  zorn2lem7  10504  ttukey2g  10518  axdc  10523  brdom3  10531  brdom5  10532  brdom4  10533  brdom7disj  10534  brdom6disj  10535  konigthlem  10577  pwfseq  10673  tsk0  10772  gruina  10827  ltbtwnnq  10987  reclem2pr  11057  supsrlem  11120  supsr  11121  axpre-sup  11178  dedekindle  11398  nnunb  12524  ioorebas  13504  fzn0  13592  fzon0  13733  axdc4uzlem  14047  hasheqf1oi  14415  hash1snb  14484  hash1n0  14486  hashf1lem2  14521  hashle2pr  14542  hashge2el2difr  14546  hashge3el3dif  14552  fi1uzind  14572  brfi1indALT  14575  swrdcl  14713  pfxcl  14747  relexpindlem  15136  fclim  15640  climmo  15644  rlimdmo1  15705  cicsym  17893  cictr  17894  brssc  17903  sscpwex  17904  initoid  18090  termoid  18091  initoeu1  18100  initoeu2lem1  18103  initoeu2  18105  termoeu1  18107  opifismgm  18751  grpidval  18754  dfgrp3e  19163  subgint  19274  giclcl  19400  gicrcl  19401  gicsym  19402  gicen  19405  gicsubgen  19406  cntzssv  19455  symgvalstruct  19524  giccyg  20027  riclcl  20660  ricrcl  20661  ricsym  20662  isbrric2  20664  ricgic  20666  subrngint  20722  subrgint  20757  abvn0b  21002  lmiclcl  21254  lmicrcl  21255  lmicsym  21256  nzerooringczr  21693  lmiclbs  22050  lmisfree  22055  lmictra  22058  mpfrcl  22301  ply1frcl  22543  pf1rcl  22574  mat1scmat  22761  toprntopon  23150  topnex  23221  neitr  23405  cmpsub  23625  bwth  23635  iunconn  23653  2ndcsb  23674  unisngl  23753  elpt  23798  ptclsg  23841  hmphsym  24008  hmphen  24011  haushmphlem  24013  cmphmph  24014  connhmph  24015  reghmph  24019  nrmhmph  24020  hmphdis  24022  indishmph  24024  hmphen2  24025  ufldom  24188  alexsubALTlem2  24274  alexsubALT  24277  metustfbas  24783  iunmbl2  25785  ioorcl2  25800  ioorinv2  25803  opnmblALT  25831  plyssc  26425  aannenlem2  26565  sltstr  28052  oncutlt  28529  istrkg2ld  28801  axcontlem4  29424  lfuhgr3  29607  lfuhgr1v0e  29714  nbgr1vtx  29818  edgusgrnbfin  29833  cplgr1vlem  29889  cplgr1v  29890  fusgrn0degnn0  29959  g0wlk0  30110  wspthneq1eq2  30328  wlkswwlksf1o  30347  wwlksnndef  30373  wspthsnonn0vne  30385  loop1cycl  30623  eulerpath  30721  frgrwopreglem2  30793  friendship  30879  shintcli  31810  strlem1  32731  rexunirn  32967  iunrnmptss  33038  lsmsnorb  33824  mxidlnzrb  33882  prsdm  34424  prsrn  34425  0elsiga  34624  sigaclcu  34627  issgon  34633  insiga  34648  omssubaddlem  34810  omssubadd  34811  bnj906  35439  bnj938  35446  bnj1018g  35472  bnj1018  35473  bnj1020  35474  bnj1125  35501  bnj1145  35502  axprALT2  35617  rankscott  35635  rankscottu  35636  fineqvac  35642  fineqvnttrclselem1  35647  fineqvnttrclselem2  35648  onvf1odlem4  35703  vonf1oonfo  35712  satfrnmapom  35949  satf0op  35956  sat1el2xp  35958  dmopab3rexdif  35984  mppspstlem  36150  txpss3v  36455  pprodss4v  36461  elsingles  36495  fnimage  36506  funpartlem  36521  funpartfun  36522  dfrdg4  36530  colinearex  36640  dfttc4  37149  ttcexg  37151  regsfromregtco  37157  bj-cleljusti  37410  axc11n11r  37416  bj-exlimvmpi  37654  bj-snglex  37717  bj-unexg  37782  bj-bm1.3ii  37808  bj-axseprep  37819  bj-restpw  37842  mptsnunlem  38092  ctbssinf  38160  pibt2  38171  wl-ax12v2cl  38260  wl-moteq  38277  wl-sbcom2d  38324  wl-mo3t  38339  ptrecube  38369  mblfinlem3  38408  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  indexdom  38484  xrnss3v  39129  prtlem16  39742  riccrng1  43403  ricdrng1  43410  sbccomieg  43634  setindtr  43865  setindtrs  43866  dfac11  43903  lnmlmic  43929  gicabl  43940  isnumbasgrplem1  43942  iscard4  44373  rtrclex  44457  clcnvlem  44463  brtrclfv2  44567  snhesn  44626  frege55b  44737  frege55c  44758  grucollcld  45084  grumnudlem  45109  iotain  45241  iotavalb  45254  sbiota1  45258  iunconnlem2  45757  permaxun  45834  permac8prim  45837  fnchoice  45863  stoweidlem59  46887  vitali2  47522  nsssmfmbf  47607  fsetprcnexALT  47950  funop1  48171  sbcpr  48421  gricen  48841  grlicsym  48929  grlictr  48931  grlicen  48933  gricgrlic  48934  usgrexmpl12ngric  48954  usgrexmpl12ngrlic  48955  opmpoismgm  49082  mo0sn  49744  mofmo  49775  mofeu  49776  f1mo  49781  eloprab1st2nd  49796  neircl  49831  sectrcl  49948  invrcl  49950  isorcl  49959  isoval2  49961  initc  50017  uobffth  50144  uobeqw  50145  fullthinc  50376  termco  50407  termcbasmo  50409  isinito3  50426  oppctermhom  50430  functermc  50434  termc2  50444  eufunclem  50447  eufunc  50448  euendfunc  50452  arweuthinc  50455  arweutermc  50456  discsntermlem  50496  rellan  50549  relran  50550  termolmd  50596  setrec1lem3  50615  elsetrecs  50626  elpglem1  50637