Theorem exlimiv 1929

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

Syntax hints:   → wi 4  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  exlimiiv  1930  exlimivv  1931  exsbim  2001  ax8  2114  ax9  2122  dfeumo  2540  mo3  2567  mo4  2569  moanimv  2622  euanv  2627  mopick  2628  clelab  2890  rexlimiva  3153  gencl  3533  cgsexg  3536  ceqsexvOLD  3543  gencbvex2  3554  vtocleg  3565  vtoclgOLD  3583  eqvincg  3661  elrabi  3703  sbcex2  3869  sbccomlem  3891  eluni  4934  intab  5002  uniintsn  5009  dfiun2g  5053  disjiun  5154  trintss  5302  axrep6g  5311  intex  5362  axpweq  5369  eunex  5408  eusvnf  5410  eusvnfb  5411  reusv2lem3  5418  unipw  5470  moabex  5479  nnullss  5482  exss  5483  sbcop1  5508  mosubopt  5529  opelopabsb  5549  relop  5875  dmopab2rex  5942  dmrnssfld  5996  dmsnopg  6244  unixp0  6314  elsnxp  6322  iotauni2  6542  iotanul2  6543  iotaex  6546  iotauni  6548  iota1  6550  iota4  6554  dffv2  7017  fveqdmss  7112  eldmrexrnb  7126  exfo  7139  funop  7183  funopdmsn  7184  funsndifnop  7185  csbriota  7420  eusvobj2  7440  fnoprabg  7573  limuni3  7889  tfindsg  7898  findsg  7937  elxp5  7963  f1oexbi  7968  ffoss  7986  fo1stres  8056  fo2ndres  8057  eloprabi  8104  frxp  8167  suppimacnv  8215  mpoxneldm  8253  mpoxopxnop0  8256  reldmtpos  8275  dftpos4  8286  frrlem2  8328  frrlem3  8329  frrlem4  8330  frrlem8  8334  wfrlem2OLD  8365  wfrlem3OLD  8366  wfrlem4OLD  8368  wfrdmclOLD  8373  wfrlem12OLD  8376  tfrlem9  8441  ecdmn0  8812  mapprc  8888  fsetprcnex  8920  ixpprc  8977  ixpn0  8988  bren  9013  brenOLD  9014  brdomg  9016  brdomgOLD  9017  domssl  9058  domssr  9059  ener  9061  en0  9078  en0OLD  9079  en0ALT  9080  en0r  9081  en1  9086  en1OLD  9087  en1b  9088  en1bOLD  9089  2dom  9095  fiprc  9111  dom0  9168  pwdom  9195  domssex  9204  ssenen  9217  rexdif1enOLD  9225  dif1en  9226  dif1enOLD  9228  findcard2s  9231  ensymfib  9250  php  9273  phpOLD  9285  sdom1  9305  1sdom2dom  9310  isinf  9323  isinfOLD  9324  en1eqsn  9336  infn0  9368  pwfir  9383  fodomfir  9396  hartogslem1  9611  brwdom  9636  brwdomn0  9638  wdompwdom  9647  unxpwdom2  9657  ixpiunwdom  9659  infeq5  9706  omex  9712  brttrcl  9782  ttrcltr  9785  dmttrcl  9790  rnttrcl  9791  epfrs  9800  rankwflemb  9862  bnd2  9962  oncard  10029  carduni  10050  pm54.43  10070  ween  10104  acnrcl  10111  acndom  10120  acndom2  10123  iunfictbso  10183  aceq3lem  10189  dfac4  10191  dfac5lem4  10195  dfac5lem5  10196  dfac5lem4OLD  10197  dfac5  10198  dfac2a  10199  dfac2b  10200  dfacacn  10211  dfac12r  10216  kmlem2  10221  kmlem16  10235  ackbij2  10311  cff  10317  cardcf  10321  cfeq0  10325  cfsuc  10326  cff1  10327  cfcoflem  10341  coftr  10342  infpssr  10377  fin4en1  10378  isfin4-2  10383  enfin2i  10390  fin23lem21  10408  fin23lem30  10411  fin23lem41  10421  enfin1ai  10453  fin1a2lem7  10475  domtriomlem  10511  axdc2lem  10517  axdc3lem2  10520  axdc4lem  10524  axcclem  10526  ac6s  10553  zorn2lem7  10571  ttukey2g  10585  axdc  10590  brdom3  10597  brdom5  10598  brdom4  10599  brdom7disj  10600  brdom6disj  10601  konigthlem  10637  pwcfsdom  10652  pwfseq  10733  tsk0  10832  gruina  10887  ltbtwnnq  11047  reclem2pr  11117  supsrlem  11180  supsr  11181  axpre-sup  11238  dedekindle  11454  nnunb  12549  ioorebas  13511  fzn0  13598  fzon0  13734  axdc4uzlem  14034  hasheqf1oi  14400  hash1snb  14468  hash1n0  14470  hashf1lem2  14505  hashle2pr  14526  hashge2el2difr  14530  hashge3el3dif  14536  fi1uzind  14556  brfi1indALT  14559  swrdcl  14693  pfxcl  14725  relexpindlem  15112  fclim  15599  climmo  15603  rlimdmo1  15664  cicsym  17865  cictr  17866  brssc  17875  sscpwex  17876  initoid  18068  termoid  18069  initoeu1  18078  initoeu2lem1  18081  initoeu2  18083  termoeu1  18085  opifismgm  18697  grpidval  18699  dfgrp3e  19080  subgint  19190  giclcl  19313  gicrcl  19314  gicsym  19315  gicen  19318  gicsubgen  19319  cntzssv  19368  symgvalstruct  19438  symgvalstructOLD  19439  giccyg  19942  brric2  20532  ricgic  20533  subrngint  20586  subrgint  20623  abvn0b  20859  lmiclcl  21092  lmicrcl  21093  lmicsym  21094  nzerooringczr  21514  lmiclbs  21880  lmisfree  21885  lmictra  21888  mpfrcl  22132  ply1frcl  22343  pf1rcl  22374  mat1scmat  22566  toprntopon  22952  topnex  23024  neitr  23209  cmpsub  23429  bwth  23439  iunconn  23457  2ndcsb  23478  unisngl  23556  elpt  23601  ptclsg  23644  hmphsym  23811  hmphen  23814  haushmphlem  23816  cmphmph  23817  connhmph  23818  reghmph  23822  nrmhmph  23823  hmphdis  23825  indishmph  23827  hmphen2  23828  ufldom  23991  alexsubALTlem2  24077  alexsubALT  24080  metustfbas  24591  iunmbl2  25611  ioorcl2  25626  ioorinv2  25629  opnmblALT  25657  plyssc  26259  aannenlem2  26389  mulog2sum  27599  sslttr  27870  istrkg2ld  28486  axcontlem4  29000  lfuhgr1v0e  29289  nbgr1vtx  29393  edgusgrnbfin  29408  cplgr1vlem  29464  cplgr1v  29465  fusgrn0degnn0  29535  g0wlk0  29688  wspthneq1eq2  29893  wlkswwlksf1o  29912  wwlksnndef  29938  wspthsnonn0vne  29950  eulerpath  30273  frgrwopreglem2  30345  friendship  30431  shintcli  31361  strlem1  32282  rexunirn  32520  iunrnmptss  32588  cnvoprabOLD  32734  lsmsnorb  33384  mxidlnzrb  33473  prsdm  33860  prsrn  33861  0elsiga  34078  sigaclcu  34081  issgon  34087  insiga  34101  omssubaddlem  34264  omssubadd  34265  bnj906  34906  bnj938  34913  bnj1018g  34939  bnj1018  34940  bnj1020  34941  bnj1125  34968  bnj1145  34969  funen1cnv  35064  fineqvac  35073  lfuhgr3  35087  loop1cycl  35105  satfrnmapom  35338  satf0op  35345  sat1el2xp  35347  dmopab3rexdif  35373  mppspstlem  35539  txpss3v  35842  pprodss4v  35848  elsingles  35882  fnimage  35893  funpartlem  35906  funpartfun  35907  dfrdg4  35915  colinearex  36024  bj-cleljusti  36645  axc11n11r  36649  bj-exlimvmpi  36877  bj-snglex  36939  bj-unexg  37004  bj-bm1.3ii  37030  bj-restpw  37058  mptsnunlem  37304  ctbssinf  37372  pibt2  37383  wl-moteq  37468  wl-sbcom2d  37515  wl-mo3t  37530  ptrecube  37580  mblfinlem3  37619  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  indexdom  37694  xrnss3v  38328  prtlem16  38825  ricsym  42474  riccrng1  42476  ricdrng1  42483  sbccomieg  42749  setindtr  42981  setindtrs  42982  dfac11  43019  lnmlmic  43045  gicabl  43056  isnumbasgrplem1  43058  iscard4  43495  rtrclex  43579  clcnvlem  43585  brtrclfv2  43689  snhesn  43748  frege55b  43859  frege55c  43880  grucollcld  44229  grumnudlem  44254  iotain  44386  iotavalb  44399  sbiota1  44403  iunconnlem2  44906  fnchoice  44929  stoweidlem59  45980  vitali2  46615  nsssmfmbf  46700  fsetprcnexALT  46977  funop1  47198  sbcpr  47395  gricen  47778  grlicsym  47830  grlictr  47832  grlicen  47834  gricgrlic  47835  usgrexmpl12ngric  47853  usgrexmpl12ngrlic  47854  opmpoismgm  47890  mo0sn  48547  mofmo  48560  mofeu  48561  f1mo  48566  neircl  48584  fullthinc  48713  setrec1lem3  48781  elsetrecs  48792  elpglem1  48803