Theorem exlimiv 1858

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

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

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

Syntax hints:   → wi 4  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  exlimiiv  1859  exlimivv  1860  equvinv  1959  equvinvOLD  1962  ax8  1996  ax9  2003  sbcom2  2445  euex  2494  mo3  2507  mopick  2535  gencl  3235  cgsexg  3238  gencbvex2  3251  vtocleg  3279  eqvincg  3329  elrabi  3359  sbcex2  3486  eluni  4439  intab  4507  uniintsn  4514  disjiun  4640  trintss  4769  intex  4820  axpweq  4842  eunex  4859  eusvnf  4861  eusvnfb  4862  reusv2lem3  4871  unipw  4918  moabex  4927  nnullss  4930  exss  4931  mosubopt  4972  opelopabsb  4985  relop  5272  dmrnssfld  5384  dmsnopg  5606  unixp0  5669  elsnxp  5677  iotauni  5863  iota1  5865  iota4  5869  dffv2  6271  fveqdmss  6354  eldmrexrnb  6366  exfo  6377  funop  6414  funopdmsn  6415  funsndifnop  6416  csbriota  6623  eusvobj2  6643  fnoprabg  6761  limuni3  7052  tfindsg  7060  findsg  7093  elxp5  7111  f1oexbi  7116  ffoss  7127  fo1stres  7192  fo2ndres  7193  eloprabi  7232  frxp  7287  suppimacnv  7306  mpt2xneldm  7338  mpt2xopxnop0  7341  reldmtpos  7360  dftpos4  7371  wfrlem2  7415  wfrlem3  7416  wfrlem4  7418  wfrdmcl  7423  wfrlem12  7426  tfrlem9  7481  ecdmn0  7789  mapprc  7861  ixpprc  7929  ixpn0  7940  bren  7964  brdomg  7965  ctex  7970  ener  8002  enerOLD  8003  en0  8019  en1  8023  en1b  8024  2dom  8029  fiprc  8039  pwdom  8112  domssex  8121  ssenen  8134  php  8144  isinf  8173  findcard2s  8201  hartogslem1  8447  brwdom  8472  brwdomn0  8474  wdompwdom  8483  unxpwdom2  8493  ixpiunwdom  8496  infeq5  8534  omex  8540  epfrs  8607  rankwflemb  8656  bnd2  8756  oncard  8786  carduni  8807  pm54.43  8826  ween  8858  acnrcl  8865  acndom  8874  acndom2  8877  iunfictbso  8937  aceq3lem  8943  dfac4  8945  dfac5lem4  8949  dfac5lem5  8950  dfac5  8951  dfac2a  8952  dfac2  8953  dfacacn  8963  dfac12r  8968  kmlem2  8973  kmlem16  8987  ackbij2  9065  cff  9070  cardcf  9074  cfeq0  9078  cfsuc  9079  cff1  9080  cfcoflem  9094  coftr  9095  infpssr  9130  fin4en1  9131  isfin4-2  9136  enfin2i  9143  fin23lem21  9161  fin23lem30  9164  fin23lem41  9174  enfin1ai  9206  fin1a2lem7  9228  domtriomlem  9264  axdc2lem  9270  axdc3lem2  9273  axdc4lem  9277  axcclem  9279  ac6s  9306  zorn2lem7  9324  ttukey2g  9338  axdc  9343  brdom3  9350  brdom5  9351  brdom4  9352  brdom7disj  9353  brdom6disj  9354  konigthlem  9390  pwcfsdom  9405  pwfseq  9486  tsk0  9585  gruina  9640  grothpw  9648  ltbtwnnq  9800  reclem2pr  9870  supsrlem  9932  supsr  9933  axpre-sup  9990  dedekindle  10201  nnunb  11288  ioorebas  12275  fzn0  12355  fzon0  12487  axdc4uzlem  12782  hasheqf1oi  13140  hasheqf1oiOLD  13141  hash1snb  13207  hash1n0  13209  hashf1lem2  13240  hashle2pr  13259  hashge2el2difr  13263  hashge3el3dif  13268  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  swrdcl  13419  relexpindlem  13803  fclim  14284  climmo  14288  rlimdmo1  14348  xpsfrnel2  16225  cicsym  16464  cictr  16465  brssc  16474  sscpwex  16475  initoid  16655  termoid  16656  initoeu1  16661  initoeu2lem1  16664  initoeu2  16666  termoeu1  16668  opifismgm  17258  grpidval  17260  dfgrp3e  17515  subgint  17618  giclcl  17714  gicrcl  17715  gicsym  17716  gicen  17720  gicsubgen  17721  cntzssv  17761  giccyg  18301  brric2  18745  ricgic  18746  subrgint  18802  lmiclcl  19070  lmicrcl  19071  lmicsym  19072  abvn0b  19302  mpfrcl  19518  ply1frcl  19683  pf1rcl  19713  lmiclbs  20176  lmisfree  20181  lmictra  20184  mat1scmat  20345  toprntopon  20729  topnex  20800  neitr  20984  cmpsub  21203  bwth  21213  iunconn  21231  2ndcsb  21252  unisngl  21330  elpt  21375  ptclsg  21418  hmphsym  21585  hmphen  21588  haushmphlem  21590  cmphmph  21591  connhmph  21592  reghmph  21596  nrmhmph  21597  hmphdis  21599  indishmph  21601  hmphen2  21602  ufldom  21766  alexsubALTlem2  21852  alexsubALT  21855  metustfbas  22362  iunmbl2  23325  ioorcl2  23340  ioorinv2  23343  opnmblALT  23371  plyssc  23956  aannenlem2  24084  mulog2sum  25226  istrkg2ld  25359  axcontlem4  25847  lfuhgr1v0e  26146  nbgr1vtx  26254  edgusgrnbfin  26275  cplgr1vlem  26325  cplgr1v  26326  fusgrn0degnn0  26395  g0wlk0  26548  wspthneq1eq2  26745  wlkpwwlkf1ouspgr  26765  wlknwwlksnsur  26776  wlkwwlksur  26783  wwlksnndef  26800  wspthsnonn0vne  26813  clwwlksnndef  26890  eulerpath  27101  frgrwopreglem2  27177  friendship  27257  shintcli  28188  strlem1  29109  rexunirn  29331  cnvoprab  29498  prsdm  29960  prsrn  29961  0elsiga  30177  sigaclcu  30180  issgon  30186  insiga  30200  omssubaddlem  30361  omssubadd  30362  bnj521  30805  bnj906  31000  bnj938  31007  bnj1018  31032  bnj1020  31033  bnj1125  31060  bnj1145  31061  mppspstlem  31468  frrlem2  31781  frrlem3  31782  frrlem4  31783  frrlem5e  31788  frrlem11  31792  sslttr  31914  txpss3v  31985  pprodss4v  31991  elsingles  32025  fnimage  32036  funpartlem  32049  funpartfun  32050  dfrdg4  32058  colinearex  32167  bj-sbex  32626  bj-cleljusti  32669  axc11n11r  32673  bj-eunex  32799  bj-mo3OLD  32832  bj-snglex  32961  bj-restpw  33045  mptsnunlem  33185  wl-sbcom2d  33344  wl-mo3t  33358  wl-ax8clv1  33378  wl-ax8clv2  33381  ptrecube  33409  mblfinlem3  33448  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  indexdom  33529  xrnss3v  34135  prtlem16  34154  sbccomieg  37357  setindtr  37591  setindtrs  37592  dfac11  37632  lnmlmic  37658  gicabl  37669  isnumbasgrplem1  37671  rtrclex  37924  clcnvlem  37930  brtrclfv2  38019  snhesn  38080  frege55b  38191  frege55c  38212  iotain  38618  iotavalb  38631  sbiota1  38635  iunconnlem2  39171  fnchoice  39188  stoweidlem59  40276  vitali2  40908  nsssmfmbf  40987  funop1  41302  pfxcl  41386  opmpt2ismgm  41807  nzerooringczr  42072  setrec1lem3  42436  elsetrecs  42445  elpglem1  42454