Theorem exlimiv 1957

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

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

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

Syntax hints:   → wi 4  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  exlimiiv  1958  exlimivv  1959  exsbim  2029  ax8  2155  ax9  2163  dfeumo  2570  mo3  2598  mo4  2600  moanimv  2653  euanv  2658  mopick  2659  clelab  2913  rexlimiva  3164  gencl  3504  cgsexg  3507  gencbvex2  3520  vtocleg  3530  eqvincg  3616  elrabi  3655  sbcex2  3813  sbccomlem  3831  eluni  4876  intab  4944  uniintsn  4951  dfiun2g  4995  disjiun  5098  trintss  5238  axrep6g  5252  sepexlem  5261  intex  5312  axpweq  5319  eunex  5359  eusvnf  5361  eusvnfb  5362  reusv2lem3  5369  axprglem  5405  axprg  5406  unipw  5429  moabex  5437  moabexOLD  5438  nnullss  5441  exss  5442  sbcop1  5468  mosubopt  5491  opelopabsb  5512  relop  5834  dmopab2rex  5905  dmrnssfld  5962  dmsnopg  6212  unixp0  6282  elsnxp  6290  iotauni2  6506  iotanul2  6507  iotaex  6510  iotauni  6511  iota1  6513  iota4  6515  dffv2  6974  fveqdmss  7071  eldmrexrnb  7085  exfo  7098  funop  7144  funopdmsn  7145  funsndifnop  7146  csbriota  7380  eusvobj2  7400  fnoprabg  7531  limuni3  7844  tfindsg  7853  findsg  7890  elxp5  7916  f1oexbi  7921  ffoss  7939  fo1stres  8008  fo2ndres  8009  eloprabi  8056  frxp  8118  suppimacnv  8166  mpoxneldm  8204  mpoxopxnop0  8207  reldmtpos  8226  dftpos4  8237  frrlem2  8280  frrlem3  8281  frrlem4  8282  frrlem8  8286  tfrlem9  8368  ecdmn0  8743  mapprc  8824  fsetprcnex  8855  ixpprc  8913  ixpn0  8924  bren  8949  brdomg  8951  domssl  8991  domssr  8992  ener  8994  en0  9011  en0ALT  9012  en0r  9013  en1  9017  en1b  9018  2dom  9023  fiprc  9037  dom0  9089  pwdom  9113  domssex  9122  ssenen  9135  dif1en  9142  findcard2s  9146  ensymfib  9164  php  9187  sdom1  9206  1sdom2dom  9210  isinf  9221  en1eqsn  9231  infn0  9258  pwfir  9272  fodomfir  9283  hartogslem1  9500  brwdom  9525  brwdomn0  9527  wdompwdom  9536  unxpwdom2  9546  ixpiunwdom  9548  elirrvOLD  9556  infeq5  9602  brttrcl  9678  ttrcltr  9681  dmttrcl  9686  rnttrcl  9687  epfrs  9696  rankwflemb  9761  bnd2  9875  oncard  9942  carduni  9963  pm54.43  9983  ween  10015  acnrcl  10022  acndom  10031  acndom2  10034  iunfictbso  10094  aceq3lem  10100  dfac4  10102  dfac5lem4  10106  dfac5lem5  10107  dfac5  10108  dfac2a  10109  dfac2b  10110  dfacacn  10121  dfac12r  10126  kmlem2  10131  kmlem16  10145  ackbij2  10221  cff  10227  cardcf  10231  cfeq0  10236  cfsuc  10237  cff1  10238  cfcoflem  10252  coftr  10253  infpssr  10288  fin4en1  10289  isfin4-2  10294  enfin2i  10301  fin23lem21  10319  fin23lem30  10322  fin23lem41  10332  enfin1ai  10364  fin1a2lem7  10386  domtriomlem  10422  axdc2lem  10428  axdc3lem2  10431  axdc4lem  10435  axcclem  10437  ac6s  10464  zorn2lem7  10482  ttukey2g  10496  axdc  10501  brdom3  10508  brdom5  10509  brdom4  10510  brdom7disj  10511  brdom6disj  10512  konigthlem  10549  pwfseq  10645  tsk0  10744  gruina  10799  ltbtwnnq  10959  reclem2pr  11029  supsrlem  11092  supsr  11093  axpre-sup  11150  dedekindle  11370  nnunb  12496  ioorebas  13474  fzn0  13562  fzon0  13702  axdc4uzlem  14015  hasheqf1oi  14383  hash1snb  14452  hash1n0  14454  hashf1lem2  14489  hashle2pr  14510  hashge2el2difr  14514  hashge3el3dif  14520  fi1uzind  14540  brfi1indALT  14543  swrdcl  14679  pfxcl  14711  relexpindlem  15096  fclim  15600  climmo  15604  rlimdmo1  15665  cicsym  17857  cictr  17858  brssc  17867  sscpwex  17868  initoid  18054  termoid  18055  initoeu1  18064  initoeu2lem1  18067  initoeu2  18069  termoeu1  18071  opifismgm  18713  grpidval  18715  dfgrp3e  19102  subgint  19213  giclcl  19339  gicrcl  19340  gicsym  19341  gicen  19344  gicsubgen  19345  cntzssv  19394  symgvalstruct  19463  giccyg  19966  ricsym  20584  brric2  20585  ricgic  20586  subrngint  20641  subrgint  20676  abvn0b  20913  lmiclcl  21165  lmicrcl  21166  lmicsym  21167  nzerooringczr  21595  lmiclbs  21952  lmisfree  21957  lmictra  21960  mpfrcl  22201  ply1frcl  22443  pf1rcl  22474  mat1scmat  22661  toprntopon  23047  topnex  23118  neitr  23302  cmpsub  23522  bwth  23532  iunconn  23550  2ndcsb  23571  unisngl  23649  elpt  23694  ptclsg  23737  hmphsym  23904  hmphen  23907  haushmphlem  23909  cmphmph  23910  connhmph  23911  reghmph  23915  nrmhmph  23916  hmphdis  23918  indishmph  23920  hmphen2  23921  ufldom  24084  alexsubALTlem2  24170  alexsubALT  24173  metustfbas  24679  iunmbl2  25681  ioorcl2  25696  ioorinv2  25699  opnmblALT  25727  plyssc  26322  aannenlem2  26455  sltstr  27942  oncutlt  28419  istrkg2ld  28691  axcontlem4  29254  lfuhgr1v0e  29541  nbgr1vtx  29645  edgusgrnbfin  29660  cplgr1vlem  29716  cplgr1v  29717  fusgrn0degnn0  29786  g0wlk0  29937  wspthneq1eq2  30146  wlkswwlksf1o  30165  wwlksnndef  30191  wspthsnonn0vne  30203  eulerpath  30529  frgrwopreglem2  30601  friendship  30687  shintcli  31618  strlem1  32539  rexunirn  32775  iunrnmptss  32847  lsmsnorb  33644  mxidlnzrb  33703  prsdm  34245  prsrn  34246  0elsiga  34445  sigaclcu  34448  issgon  34454  insiga  34468  omssubaddlem  34630  omssubadd  34631  bnj906  35259  bnj938  35266  bnj1018g  35292  bnj1018  35293  bnj1020  35294  bnj1125  35321  bnj1145  35322  funen1cnv  35416  axprALT2  35441  fineqvac  35448  fineqvnttrclselem1  35453  fineqvnttrclselem2  35454  onvf1odlem4  35485  vonf1oonfo  35494  lfuhgr3  35507  loop1cycl  35524  satfrnmapom  35757  satf0op  35764  sat1el2xp  35766  dmopab3rexdif  35792  mppspstlem  35958  txpss3v  36263  pprodss4v  36269  elsingles  36303  fnimage  36314  funpartlem  36329  funpartfun  36330  dfrdg4  36338  colinearex  36447  dfttc4  36926  ttcexg  36928  regsfromregtco  36934  bj-cleljusti  37187  axc11n11r  37193  bj-exlimvmpi  37431  bj-snglex  37493  bj-unexg  37558  bj-bm1.3ii  37584  bj-axseprep  37594  bj-restpw  37617  mptsnunlem  37867  ctbssinf  37935  pibt2  37946  wl-ax12v2cl  38035  wl-moteq  38052  wl-sbcom2d  38099  wl-mo3t  38114  ptrecube  38154  mblfinlem3  38193  ovoliunnfl  38196  voliunnfl  38198  volsupnfl  38199  indexdom  38268  xrnss3v  38915  prtlem16  39528  riccrng1  43176  ricdrng1  43183  sbccomieg  43407  setindtr  43638  setindtrs  43639  dfac11  43676  lnmlmic  43702  gicabl  43713  isnumbasgrplem1  43715  iscard4  44146  rtrclex  44230  clcnvlem  44236  brtrclfv2  44340  snhesn  44399  frege55b  44510  frege55c  44531  grucollcld  44857  grumnudlem  44882  iotain  45014  iotavalb  45027  sbiota1  45031  iunconnlem2  45530  permaxun  45607  permac8prim  45610  fnchoice  45636  stoweidlem59  46660  vitali2  47295  nsssmfmbf  47380  fsetprcnexALT  47683  funop1  47904  sbcpr  48154  gricen  48574  grlicsym  48662  grlictr  48664  grlicen  48666  gricgrlic  48667  usgrexmpl12ngric  48687  usgrexmpl12ngrlic  48688  opmpoismgm  48816  mo0sn  49474  mofmo  49505  mofeu  49506  f1mo  49511  eloprab1st2nd  49526  neircl  49563  sectrcl  49680  invrcl  49682  isorcl  49691  isoval2  49693  initc  49749  uobffth  49876  uobeqw  49877  fullthinc  50108  termco  50139  termcbasmo  50141  isinito3  50158  oppctermhom  50162  functermc  50166  termc2  50176  eufunclem  50179  eufunc  50180  euendfunc  50184  arweuthinc  50187  arweutermc  50188  discsntermlem  50228  rellan  50281  relran  50282  termolmd  50328  setrec1lem3  50347  elsetrecs  50358  elpglem1  50369