Theorem exlimiv 1931

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

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

This inference, along with its many variants such as rexlimdv 3131, 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 3131. 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 2113. (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  2117  ax9  2125  dfeumo  2532  mo3  2559  mo4  2561  moanimv  2614  euanv  2619  mopick  2620  clelab  2876  rexlimiva  3125  gencl  3478  cgsexg  3481  gencbvex2  3496  vtocleg  3506  eqvincg  3598  elrabi  3638  sbcex2  3797  sbccomlem  3815  eluni  4857  intab  4923  uniintsn  4930  dfiun2g  4975  disjiun  5074  trintss  5211  axrep6g  5223  sepexlem  5232  intex  5277  axpweq  5284  eunex  5323  eusvnf  5325  eusvnfb  5326  reusv2lem3  5333  unipw  5386  moabex  5394  nnullss  5397  exss  5398  sbcop1  5423  mosubopt  5445  opelopabsb  5465  relop  5785  dmopab2rex  5852  dmrnssfld  5908  dmsnopg  6155  unixp0  6225  elsnxp  6233  iotauni2  6448  iotanul2  6449  iotaex  6452  iotauni  6453  iota1  6455  iota4  6457  dffv2  6912  fveqdmss  7006  eldmrexrnb  7020  exfo  7033  funop  7077  funopdmsn  7078  funsndifnop  7079  csbriota  7313  eusvobj2  7333  fnoprabg  7464  limuni3  7777  tfindsg  7786  findsg  7822  elxp5  7848  f1oexbi  7853  ffoss  7873  fo1stres  7942  fo2ndres  7943  eloprabi  7990  frxp  8051  suppimacnv  8099  mpoxneldm  8137  mpoxopxnop0  8140  reldmtpos  8159  dftpos4  8170  frrlem2  8212  frrlem3  8213  frrlem4  8214  frrlem8  8218  tfrlem9  8299  ecdmn0  8669  mapprc  8749  fsetprcnex  8781  ixpprc  8838  ixpn0  8849  bren  8874  brdomg  8876  domssl  8915  domssr  8916  ener  8918  en0  8935  en0ALT  8936  en0r  8937  en1  8941  en1b  8942  2dom  8947  fiprc  8961  dom0  9013  pwdom  9037  domssex  9046  ssenen  9059  dif1en  9066  findcard2s  9070  ensymfib  9088  php  9111  sdom1  9129  1sdom2dom  9133  isinf  9144  en1eqsn  9154  infn0  9181  pwfir  9196  fodomfir  9207  hartogslem1  9423  brwdom  9448  brwdomn0  9450  wdompwdom  9459  unxpwdom2  9469  ixpiunwdom  9471  elirrv  9478  infeq5  9522  brttrcl  9598  ttrcltr  9601  dmttrcl  9606  rnttrcl  9607  epfrs  9616  rankwflemb  9681  bnd2  9781  oncard  9848  carduni  9869  pm54.43  9889  ween  9921  acnrcl  9928  acndom  9937  acndom2  9940  iunfictbso  10000  aceq3lem  10006  dfac4  10008  dfac5lem4  10012  dfac5lem5  10013  dfac5lem4OLD  10014  dfac5  10015  dfac2a  10016  dfac2b  10017  dfacacn  10028  dfac12r  10033  kmlem2  10038  kmlem16  10052  ackbij2  10128  cff  10134  cardcf  10138  cfeq0  10142  cfsuc  10143  cff1  10144  cfcoflem  10158  coftr  10159  infpssr  10194  fin4en1  10195  isfin4-2  10200  enfin2i  10207  fin23lem21  10225  fin23lem30  10228  fin23lem41  10238  enfin1ai  10270  fin1a2lem7  10292  domtriomlem  10328  axdc2lem  10334  axdc3lem2  10337  axdc4lem  10341  axcclem  10343  ac6s  10370  zorn2lem7  10388  ttukey2g  10402  axdc  10407  brdom3  10414  brdom5  10415  brdom4  10416  brdom7disj  10417  brdom6disj  10418  konigthlem  10454  pwfseq  10550  tsk0  10649  gruina  10704  ltbtwnnq  10864  reclem2pr  10934  supsrlem  10997  supsr  10998  axpre-sup  11055  dedekindle  11272  nnunb  12372  ioorebas  13346  fzn0  13433  fzon0  13572  axdc4uzlem  13885  hasheqf1oi  14253  hash1snb  14321  hash1n0  14323  hashf1lem2  14358  hashle2pr  14379  hashge2el2difr  14383  hashge3el3dif  14389  fi1uzind  14409  brfi1indALT  14412  swrdcl  14548  pfxcl  14580  relexpindlem  14965  fclim  15455  climmo  15459  rlimdmo1  15520  cicsym  17706  cictr  17707  brssc  17716  sscpwex  17717  initoid  17903  termoid  17904  initoeu1  17913  initoeu2lem1  17916  initoeu2  17918  termoeu1  17920  opifismgm  18562  grpidval  18564  dfgrp3e  18948  subgint  19058  giclcl  19180  gicrcl  19181  gicsym  19182  gicen  19185  gicsubgen  19186  cntzssv  19235  symgvalstruct  19304  giccyg  19807  brric2  20416  ricgic  20417  subrngint  20470  subrgint  20505  abvn0b  20746  lmiclcl  20999  lmicrcl  21000  lmicsym  21001  nzerooringczr  21412  lmiclbs  21769  lmisfree  21774  lmictra  21777  mpfrcl  22015  ply1frcl  22228  pf1rcl  22259  mat1scmat  22449  toprntopon  22835  topnex  22906  neitr  23090  cmpsub  23310  bwth  23320  iunconn  23338  2ndcsb  23359  unisngl  23437  elpt  23482  ptclsg  23525  hmphsym  23692  hmphen  23695  haushmphlem  23697  cmphmph  23698  connhmph  23699  reghmph  23703  nrmhmph  23704  hmphdis  23706  indishmph  23708  hmphen2  23709  ufldom  23872  alexsubALTlem2  23958  alexsubALT  23961  metustfbas  24467  iunmbl2  25480  ioorcl2  25495  ioorinv2  25498  opnmblALT  25526  plyssc  26127  aannenlem2  26259  sslttr  27743  onscutlt  28196  istrkg2ld  28433  axcontlem4  28940  lfuhgr1v0e  29227  nbgr1vtx  29331  edgusgrnbfin  29346  cplgr1vlem  29402  cplgr1v  29403  fusgrn0degnn0  29473  g0wlk0  29624  wspthneq1eq2  29833  wlkswwlksf1o  29852  wwlksnndef  29878  wspthsnonn0vne  29890  eulerpath  30213  frgrwopreglem2  30285  friendship  30371  shintcli  31301  strlem1  32222  rexunirn  32463  iunrnmptss  32537  lsmsnorb  33348  mxidlnzrb  33437  prsdm  33919  prsrn  33920  0elsiga  34119  sigaclcu  34122  issgon  34128  insiga  34142  omssubaddlem  34304  omssubadd  34305  bnj906  34934  bnj938  34941  bnj1018g  34967  bnj1018  34968  bnj1020  34969  bnj1125  34996  bnj1145  34997  funen1cnv  35092  fineqvac  35131  fineqvnttrclselem1  35133  fineqvnttrclselem2  35134  onvf1odlem4  35142  lfuhgr3  35156  loop1cycl  35173  satfrnmapom  35406  satf0op  35413  sat1el2xp  35415  dmopab3rexdif  35441  mppspstlem  35607  txpss3v  35912  pprodss4v  35918  elsingles  35952  fnimage  35963  funpartlem  35976  funpartfun  35977  dfrdg4  35985  colinearex  36094  bj-cleljusti  36713  axc11n11r  36717  bj-exlimvmpi  36945  bj-snglex  37007  bj-unexg  37072  bj-bm1.3ii  37098  bj-restpw  37126  mptsnunlem  37372  ctbssinf  37440  pibt2  37451  wl-ax12v2cl  37540  wl-moteq  37548  wl-sbcom2d  37595  wl-mo3t  37610  ptrecube  37660  mblfinlem3  37699  ovoliunnfl  37702  voliunnfl  37704  volsupnfl  37705  indexdom  37774  xrnss3v  38400  prtlem16  38908  ricsym  42552  riccrng1  42554  ricdrng1  42561  sbccomieg  42826  setindtr  43057  setindtrs  43058  dfac11  43095  lnmlmic  43121  gicabl  43132  isnumbasgrplem1  43134  iscard4  43566  rtrclex  43650  clcnvlem  43656  brtrclfv2  43760  snhesn  43819  frege55b  43930  frege55c  43951  grucollcld  44293  grumnudlem  44318  iotain  44450  iotavalb  44463  sbiota1  44467  iunconnlem2  44967  permaxun  45044  permac8prim  45047  fnchoice  45066  stoweidlem59  46097  vitali2  46732  nsssmfmbf  46817  fsetprcnexALT  47093  funop1  47314  sbcpr  47552  gricen  47956  grlicsym  48044  grlictr  48046  grlicen  48048  gricgrlic  48049  usgrexmpl12ngric  48069  usgrexmpl12ngrlic  48070  opmpoismgm  48198  mo0sn  48847  mofmo  48878  mofeu  48879  f1mo  48884  eloprab1st2nd  48899  neircl  48936  sectrcl  49054  invrcl  49056  isorcl  49065  isoval2  49067  initc  49123  uobffth  49250  uobeqw  49251  fullthinc  49482  termco  49513  termcbasmo  49515  isinito3  49532  oppctermhom  49536  functermc  49540  termc2  49550  eufunclem  49553  eufunc  49554  euendfunc  49558  arweuthinc  49561  arweutermc  49562  discsntermlem  49602  rellan  49655  relran  49656  termolmd  49702  setrec1lem3  49721  elsetrecs  49732  elpglem1  49743