Theorem exlimiv 1930

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

See exlimi 2218 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 1930 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1931. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1967 and ax-8 2111. (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 1835	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
3		ax5e 1912	. 2 ⊢ (∃𝑥𝜓 → 𝜓)
4	2, 3	syl 17	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  exlimiiv  1931  exlimivv  1932  exsbim  2002  ax8  2115  ax9  2123  dfeumo  2530  mo3  2557  mo4  2559  moanimv  2612  euanv  2617  mopick  2618  clelab  2873  rexlimiva  3126  gencl  3486  cgsexg  3489  gencbvex2  3505  vtocleg  3516  vtoclgOLD  3534  eqvincg  3611  elrabi  3651  sbcex2  3811  sbccomlem  3829  eluni  4870  intab  4938  uniintsn  4945  dfiun2g  4990  disjiun  5090  trintss  5228  axrep6g  5240  sepexlem  5249  intex  5294  axpweq  5301  eunex  5340  eusvnf  5342  eusvnfb  5343  reusv2lem3  5350  unipw  5405  moabex  5414  nnullss  5417  exss  5418  sbcop1  5443  mosubopt  5465  opelopabsb  5485  relop  5804  dmopab2rex  5871  dmrnssfld  5926  dmsnopg  6174  unixp0  6244  elsnxp  6252  iotauni2  6468  iotanul2  6469  iotaex  6472  iotauni  6474  iota1  6476  iota4  6480  dffv2  6938  fveqdmss  7032  eldmrexrnb  7046  exfo  7059  funop  7103  funopdmsn  7104  funsndifnop  7105  csbriota  7341  eusvobj2  7361  fnoprabg  7492  limuni3  7808  tfindsg  7817  findsg  7853  elxp5  7879  f1oexbi  7884  ffoss  7904  fo1stres  7973  fo2ndres  7974  eloprabi  8021  frxp  8082  suppimacnv  8130  mpoxneldm  8168  mpoxopxnop0  8171  reldmtpos  8190  dftpos4  8201  frrlem2  8243  frrlem3  8244  frrlem4  8245  frrlem8  8249  tfrlem9  8330  ecdmn0  8700  mapprc  8780  fsetprcnex  8812  ixpprc  8869  ixpn0  8880  bren  8905  brdomg  8907  domssl  8946  domssr  8947  ener  8949  en0  8966  en0ALT  8967  en0r  8968  en1  8972  en1b  8973  2dom  8978  fiprc  8993  dom0  9046  pwdom  9070  domssex  9079  ssenen  9092  rexdif1enOLD  9100  dif1en  9101  dif1enOLD  9103  findcard2s  9106  ensymfib  9125  php  9148  sdom1  9166  1sdom2dom  9170  isinf  9183  isinfOLD  9184  en1eqsn  9195  infn0  9227  pwfir  9242  fodomfir  9255  hartogslem1  9471  brwdom  9496  brwdomn0  9498  wdompwdom  9507  unxpwdom2  9517  ixpiunwdom  9519  infeq5  9566  brttrcl  9642  ttrcltr  9645  dmttrcl  9650  rnttrcl  9651  epfrs  9660  rankwflemb  9722  bnd2  9822  oncard  9889  carduni  9910  pm54.43  9930  ween  9964  acnrcl  9971  acndom  9980  acndom2  9983  iunfictbso  10043  aceq3lem  10049  dfac4  10051  dfac5lem4  10055  dfac5lem5  10056  dfac5lem4OLD  10057  dfac5  10058  dfac2a  10059  dfac2b  10060  dfacacn  10071  dfac12r  10076  kmlem2  10081  kmlem16  10095  ackbij2  10171  cff  10177  cardcf  10181  cfeq0  10185  cfsuc  10186  cff1  10187  cfcoflem  10201  coftr  10202  infpssr  10237  fin4en1  10238  isfin4-2  10243  enfin2i  10250  fin23lem21  10268  fin23lem30  10271  fin23lem41  10281  enfin1ai  10313  fin1a2lem7  10335  domtriomlem  10371  axdc2lem  10377  axdc3lem2  10380  axdc4lem  10384  axcclem  10386  ac6s  10413  zorn2lem7  10431  ttukey2g  10445  axdc  10450  brdom3  10457  brdom5  10458  brdom4  10459  brdom7disj  10460  brdom6disj  10461  konigthlem  10497  pwfseq  10593  tsk0  10692  gruina  10747  ltbtwnnq  10907  reclem2pr  10977  supsrlem  11040  supsr  11041  axpre-sup  11098  dedekindle  11314  nnunb  12414  ioorebas  13388  fzn0  13475  fzon0  13614  axdc4uzlem  13924  hasheqf1oi  14292  hash1snb  14360  hash1n0  14362  hashf1lem2  14397  hashle2pr  14418  hashge2el2difr  14422  hashge3el3dif  14428  fi1uzind  14448  brfi1indALT  14451  swrdcl  14586  pfxcl  14618  relexpindlem  15005  fclim  15495  climmo  15499  rlimdmo1  15560  cicsym  17742  cictr  17743  brssc  17752  sscpwex  17753  initoid  17939  termoid  17940  initoeu1  17949  initoeu2lem1  17952  initoeu2  17954  termoeu1  17956  opifismgm  18562  grpidval  18564  dfgrp3e  18948  subgint  19058  giclcl  19181  gicrcl  19182  gicsym  19183  gicen  19186  gicsubgen  19187  cntzssv  19236  symgvalstruct  19303  giccyg  19806  brric2  20391  ricgic  20392  subrngint  20445  subrgint  20480  abvn0b  20721  lmiclcl  20953  lmicrcl  20954  lmicsym  20955  nzerooringczr  21366  lmiclbs  21722  lmisfree  21727  lmictra  21730  mpfrcl  21968  ply1frcl  22181  pf1rcl  22212  mat1scmat  22402  toprntopon  22788  topnex  22859  neitr  23043  cmpsub  23263  bwth  23273  iunconn  23291  2ndcsb  23312  unisngl  23390  elpt  23435  ptclsg  23478  hmphsym  23645  hmphen  23648  haushmphlem  23650  cmphmph  23651  connhmph  23652  reghmph  23656  nrmhmph  23657  hmphdis  23659  indishmph  23661  hmphen2  23662  ufldom  23825  alexsubALTlem2  23911  alexsubALT  23914  metustfbas  24421  iunmbl2  25434  ioorcl2  25449  ioorinv2  25452  opnmblALT  25480  plyssc  26081  aannenlem2  26213  sslttr  27695  onscutlt  28141  istrkg2ld  28363  axcontlem4  28870  lfuhgr1v0e  29157  nbgr1vtx  29261  edgusgrnbfin  29276  cplgr1vlem  29332  cplgr1v  29333  fusgrn0degnn0  29403  g0wlk0  29554  wspthneq1eq2  29763  wlkswwlksf1o  29782  wwlksnndef  29808  wspthsnonn0vne  29820  eulerpath  30143  frgrwopreglem2  30215  friendship  30301  shintcli  31231  strlem1  32152  rexunirn  32394  iunrnmptss  32467  lsmsnorb  33335  mxidlnzrb  33424  prsdm  33877  prsrn  33878  0elsiga  34077  sigaclcu  34080  issgon  34086  insiga  34100  omssubaddlem  34263  omssubadd  34264  bnj906  34893  bnj938  34900  bnj1018g  34926  bnj1018  34927  bnj1020  34928  bnj1125  34955  bnj1145  34956  funen1cnv  35051  fineqvac  35060  onvf1odlem4  35066  lfuhgr3  35080  loop1cycl  35097  satfrnmapom  35330  satf0op  35337  sat1el2xp  35339  dmopab3rexdif  35365  mppspstlem  35531  txpss3v  35839  pprodss4v  35845  elsingles  35879  fnimage  35890  funpartlem  35903  funpartfun  35904  dfrdg4  35912  colinearex  36021  bj-cleljusti  36640  axc11n11r  36644  bj-exlimvmpi  36872  bj-snglex  36934  bj-unexg  36999  bj-bm1.3ii  37025  bj-restpw  37053  mptsnunlem  37299  ctbssinf  37367  pibt2  37378  wl-ax12v2cl  37467  wl-moteq  37475  wl-sbcom2d  37522  wl-mo3t  37537  ptrecube  37587  mblfinlem3  37626  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  indexdom  37701  xrnss3v  38327  prtlem16  38835  ricsym  42480  riccrng1  42482  ricdrng1  42489  sbccomieg  42754  setindtr  42986  setindtrs  42987  dfac11  43024  lnmlmic  43050  gicabl  43061  isnumbasgrplem1  43063  iscard4  43495  rtrclex  43579  clcnvlem  43585  brtrclfv2  43689  snhesn  43748  frege55b  43859  frege55c  43880  grucollcld  44222  grumnudlem  44247  iotain  44379  iotavalb  44392  sbiota1  44396  iunconnlem2  44897  permaxun  44974  permac8prim  44977  fnchoice  44996  stoweidlem59  46030  vitali2  46665  nsssmfmbf  46750  fsetprcnexALT  47036  funop1  47257  sbcpr  47495  gricen  47898  grlicsym  47978  grlictr  47980  grlicen  47982  gricgrlic  47983  usgrexmpl12ngric  48002  usgrexmpl12ngrlic  48003  opmpoismgm  48128  mo0sn  48777  mofmo  48808  mofeu  48809  f1mo  48814  eloprab1st2nd  48829  neircl  48866  sectrcl  48984  invrcl  48986  isorcl  48995  isoval2  48997  initc  49053  uobffth  49180  uobeqw  49181  fullthinc  49412  termco  49443  termcbasmo  49445  isinito3  49462  oppctermhom  49466  functermc  49470  termc2  49480  eufunclem  49483  eufunc  49484  euendfunc  49488  arweuthinc  49491  arweutermc  49492  discsntermlem  49532  rellan  49585  relran  49586  termolmd  49632  setrec1lem3  49651  elsetrecs  49662  elpglem1  49673