Theorem exlimiv 1931

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

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

This inference, along with its many variants such as rexlimdv 3283, 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 3283. 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 1970 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 1835	. 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 209  df-ex 1781

This theorem is referenced by:  exlimiiv  1932  exlimivv  1933  exsbim  2008  spsbeOLD  2089  ax8  2120  ax9  2128  dfeumo  2619  mo3  2648  mo4  2650  moanimv  2704  euanv  2709  mopick  2710  gencl  3534  cgsexg  3537  gencbvex2  3550  vtoclg  3567  vtocleg  3581  eqvincg  3641  elrabi  3675  sbcex2  3834  eluni  4841  intab  4906  uniintsn  4913  disjiun  5053  trintss  5189  intex  5240  axpweq  5265  eunex  5291  eusvnf  5293  eusvnfb  5294  reusv2lem3  5301  unipw  5343  moabex  5351  nnullss  5354  exss  5355  sbcop1  5379  mosubopt  5400  opelopabsb  5417  relop  5721  dmopab2rex  5786  dmrnssfld  5841  dmsnopg  6070  unixp0  6134  elsnxp  6142  iotauni  6330  iota1  6332  iota4  6336  dffv2  6756  fveqdmss  6846  eldmrexrnb  6858  exfo  6871  funop  6911  funopdmsn  6912  funsndifnop  6913  csbriota  7129  eusvobj2  7149  fnoprabg  7275  limuni3  7567  tfindsg  7575  findsg  7609  elxp5  7628  f1oexbi  7633  ffoss  7647  fo1stres  7715  fo2ndres  7716  eloprabi  7761  frxp  7820  suppimacnv  7841  mpoxneldm  7878  mpoxopxnop0  7881  reldmtpos  7900  dftpos4  7911  wfrlem2  7955  wfrlem3  7956  wfrlem4  7958  wfrdmcl  7963  wfrlem12  7966  tfrlem9  8021  ecdmn0  8336  mapprc  8410  ixpprc  8483  ixpn0  8494  bren  8518  brdomg  8519  ener  8556  en0  8572  en1  8576  en1b  8577  2dom  8582  fiprc  8595  pwdom  8669  domssex  8678  ssenen  8691  php  8701  isinf  8731  findcard2s  8759  hartogslem1  9006  brwdom  9031  brwdomn0  9033  wdompwdom  9042  unxpwdom2  9052  ixpiunwdom  9055  infeq5  9100  omex  9106  epfrs  9173  rankwflemb  9222  bnd2  9322  oncard  9389  carduni  9410  pm54.43  9429  ween  9461  acnrcl  9468  acndom  9477  acndom2  9480  iunfictbso  9540  aceq3lem  9546  dfac4  9548  dfac5lem4  9552  dfac5lem5  9553  dfac5  9554  dfac2a  9555  dfac2b  9556  dfacacn  9567  dfac12r  9572  kmlem2  9577  kmlem16  9591  ackbij2  9665  cff  9670  cardcf  9674  cfeq0  9678  cfsuc  9679  cff1  9680  cfcoflem  9694  coftr  9695  infpssr  9730  fin4en1  9731  isfin4-2  9736  enfin2i  9743  fin23lem21  9761  fin23lem30  9764  fin23lem41  9774  enfin1ai  9806  fin1a2lem7  9828  domtriomlem  9864  axdc2lem  9870  axdc3lem2  9873  axdc4lem  9877  axcclem  9879  ac6s  9906  zorn2lem7  9924  ttukey2g  9938  axdc  9943  brdom3  9950  brdom5  9951  brdom4  9952  brdom7disj  9953  brdom6disj  9954  konigthlem  9990  pwcfsdom  10005  pwfseq  10086  tsk0  10185  gruina  10240  ltbtwnnq  10400  reclem2pr  10470  supsrlem  10533  supsr  10534  axpre-sup  10591  dedekindle  10804  nnunb  11894  ioorebas  12840  fzn0  12922  fzon0  13056  axdc4uzlem  13352  hasheqf1oi  13713  hash1snb  13781  hash1n0  13783  hashf1lem2  13815  hashle2pr  13836  hashge2el2difr  13840  hashge3el3dif  13845  fi1uzind  13856  brfi1indALT  13859  swrdcl  14007  pfxcl  14039  relexpindlem  14422  fclim  14910  climmo  14914  rlimdmo1  14974  cicsym  17074  cictr  17075  brssc  17084  sscpwex  17085  initoid  17265  termoid  17266  initoeu1  17271  initoeu2lem1  17274  initoeu2  17276  termoeu1  17278  opifismgm  17869  grpidval  17871  dfgrp3e  18199  subgint  18303  giclcl  18412  gicrcl  18413  gicsym  18414  gicen  18417  gicsubgen  18418  cntzssv  18458  symgvalstruct  18525  giccyg  19020  brric2  19500  ricgic  19501  subrgint  19557  lmiclcl  19842  lmicrcl  19843  lmicsym  19844  abvn0b  20075  mpfrcl  20298  ply1frcl  20481  pf1rcl  20512  lmiclbs  20981  lmisfree  20986  lmictra  20989  mat1scmat  21148  toprntopon  21533  topnex  21604  neitr  21788  cmpsub  22008  bwth  22018  iunconn  22036  2ndcsb  22057  unisngl  22135  elpt  22180  ptclsg  22223  hmphsym  22390  hmphen  22393  haushmphlem  22395  cmphmph  22396  connhmph  22397  reghmph  22401  nrmhmph  22402  hmphdis  22404  indishmph  22406  hmphen2  22407  ufldom  22570  alexsubALTlem2  22656  alexsubALT  22659  metustfbas  23167  iunmbl2  24158  ioorcl2  24173  ioorinv2  24176  opnmblALT  24204  plyssc  24790  aannenlem2  24918  mulog2sum  26113  istrkg2ld  26246  axcontlem4  26753  lfuhgr1v0e  27036  nbgr1vtx  27140  edgusgrnbfin  27155  cplgr1vlem  27211  cplgr1v  27212  fusgrn0degnn0  27281  g0wlk0  27433  wspthneq1eq2  27638  wlkswwlksf1o  27657  wwlksnndef  27683  wspthsnonn0vne  27696  eulerpath  28020  frgrwopreglem2  28092  friendship  28178  shintcli  29106  strlem1  30027  rexunirn  30256  iunrnmptss  30317  cnvoprabOLD  30456  lsmsnorb  30945  mxidlnzrb  30981  prsdm  31157  prsrn  31158  0elsiga  31373  sigaclcu  31376  issgon  31382  insiga  31396  omssubaddlem  31557  omssubadd  31558  bnj521  32007  bnj906  32202  bnj938  32209  bnj1018g  32235  bnj1018  32236  bnj1020  32237  bnj1125  32264  bnj1145  32265  funen1cnv  32357  lfuhgr3  32366  loop1cycl  32384  satfrnmapom  32617  satf0op  32624  sat1el2xp  32626  dmopab3rexdif  32652  mppspstlem  32818  frrlem2  33124  frrlem3  33125  frrlem4  33126  frrlem8  33130  sslttr  33268  txpss3v  33339  pprodss4v  33345  elsingles  33379  fnimage  33390  funpartlem  33403  funpartfun  33404  dfrdg4  33412  colinearex  33521  bj-cleljusti  34013  axc11n11r  34017  bj-exlimvmpi  34230  bj-snglex  34288  bj-bm1.3ii  34360  bj-restpw  34386  mptsnunlem  34622  ctbssinf  34690  pibt2  34701  wl-moteq  34769  wl-sbcom2d  34812  wl-mo3t  34827  ptrecube  34907  mblfinlem3  34946  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  indexdom  35024  xrnss3v  35639  prtlem16  36020  sbccomieg  39439  setindtr  39670  setindtrs  39671  dfac11  39711  lnmlmic  39737  gicabl  39748  isnumbasgrplem1  39750  iscard4  39949  rtrclex  40026  clcnvlem  40032  brtrclfv2  40121  snhesn  40181  frege55b  40292  frege55c  40313  grucollcld  40645  grumnudlem  40670  iotain  40798  iotavalb  40811  sbiota1  40815  iunconnlem2  41318  fnchoice  41335  stoweidlem59  42393  vitali2  43025  nsssmfmbf  43104  funop1  43531  sbcpr  43732  opmpoismgm  44123  nzerooringczr  44392  setrec1lem3  44841  elsetrecs  44851  elpglem1  44862