Theorem exlimiv 1930

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  exlimiiv  1931  exlimivv  1932  exsbim  2002  ax8  2115  ax9  2123  dfeumo  2530  mo3  2557  mo4  2559  moanimv  2612  euanv  2617  mopick  2618  clelab  2873  rexlimiva  3126  gencl  3489  cgsexg  3492  gencbvex2  3508  vtocleg  3519  vtoclgOLD  3537  eqvincg  3614  elrabi  3654  sbcex2  3814  sbccomlem  3832  eluni  4874  intab  4942  uniintsn  4949  dfiun2g  4994  disjiun  5095  trintss  5233  axrep6g  5245  sepexlem  5254  intex  5299  axpweq  5306  eunex  5345  eusvnf  5347  eusvnfb  5348  reusv2lem3  5355  unipw  5410  moabex  5419  nnullss  5422  exss  5423  sbcop1  5448  mosubopt  5470  opelopabsb  5490  relop  5814  dmopab2rex  5881  dmrnssfld  5937  dmsnopg  6186  unixp0  6256  elsnxp  6264  iotauni2  6480  iotanul2  6481  iotaex  6484  iotauni  6486  iota1  6488  iota4  6492  dffv2  6956  fveqdmss  7050  eldmrexrnb  7064  exfo  7077  funop  7121  funopdmsn  7122  funsndifnop  7123  csbriota  7359  eusvobj2  7379  fnoprabg  7512  limuni3  7828  tfindsg  7837  findsg  7873  elxp5  7899  f1oexbi  7904  ffoss  7924  fo1stres  7994  fo2ndres  7995  eloprabi  8042  frxp  8105  suppimacnv  8153  mpoxneldm  8191  mpoxopxnop0  8194  reldmtpos  8213  dftpos4  8224  frrlem2  8266  frrlem3  8267  frrlem4  8268  frrlem8  8272  tfrlem9  8353  ecdmn0  8723  mapprc  8803  fsetprcnex  8835  ixpprc  8892  ixpn0  8903  bren  8928  brdomg  8930  domssl  8969  domssr  8970  ener  8972  en0  8989  en0ALT  8990  en0r  8991  en1  8995  en1b  8996  2dom  9001  fiprc  9016  dom0  9069  pwdom  9093  domssex  9102  ssenen  9115  rexdif1enOLD  9123  dif1en  9124  dif1enOLD  9126  findcard2s  9129  ensymfib  9148  php  9171  sdom1  9189  1sdom2dom  9194  isinf  9207  isinfOLD  9208  en1eqsn  9219  infn0  9251  pwfir  9266  fodomfir  9279  hartogslem1  9495  brwdom  9520  brwdomn0  9522  wdompwdom  9531  unxpwdom2  9541  ixpiunwdom  9543  infeq5  9590  brttrcl  9666  ttrcltr  9669  dmttrcl  9674  rnttrcl  9675  epfrs  9684  rankwflemb  9746  bnd2  9846  oncard  9913  carduni  9934  pm54.43  9954  ween  9988  acnrcl  9995  acndom  10004  acndom2  10007  iunfictbso  10067  aceq3lem  10073  dfac4  10075  dfac5lem4  10079  dfac5lem5  10080  dfac5lem4OLD  10081  dfac5  10082  dfac2a  10083  dfac2b  10084  dfacacn  10095  dfac12r  10100  kmlem2  10105  kmlem16  10119  ackbij2  10195  cff  10201  cardcf  10205  cfeq0  10209  cfsuc  10210  cff1  10211  cfcoflem  10225  coftr  10226  infpssr  10261  fin4en1  10262  isfin4-2  10267  enfin2i  10274  fin23lem21  10292  fin23lem30  10295  fin23lem41  10305  enfin1ai  10337  fin1a2lem7  10359  domtriomlem  10395  axdc2lem  10401  axdc3lem2  10404  axdc4lem  10408  axcclem  10410  ac6s  10437  zorn2lem7  10455  ttukey2g  10469  axdc  10474  brdom3  10481  brdom5  10482  brdom4  10483  brdom7disj  10484  brdom6disj  10485  konigthlem  10521  pwfseq  10617  tsk0  10716  gruina  10771  ltbtwnnq  10931  reclem2pr  11001  supsrlem  11064  supsr  11065  axpre-sup  11122  dedekindle  11338  nnunb  12438  ioorebas  13412  fzn0  13499  fzon0  13638  axdc4uzlem  13948  hasheqf1oi  14316  hash1snb  14384  hash1n0  14386  hashf1lem2  14421  hashle2pr  14442  hashge2el2difr  14446  hashge3el3dif  14452  fi1uzind  14472  brfi1indALT  14475  swrdcl  14610  pfxcl  14642  relexpindlem  15029  fclim  15519  climmo  15523  rlimdmo1  15584  cicsym  17766  cictr  17767  brssc  17776  sscpwex  17777  initoid  17963  termoid  17964  initoeu1  17973  initoeu2lem1  17976  initoeu2  17978  termoeu1  17980  opifismgm  18586  grpidval  18588  dfgrp3e  18972  subgint  19082  giclcl  19205  gicrcl  19206  gicsym  19207  gicen  19210  gicsubgen  19211  cntzssv  19260  symgvalstruct  19327  giccyg  19830  brric2  20415  ricgic  20416  subrngint  20469  subrgint  20504  abvn0b  20745  lmiclcl  20977  lmicrcl  20978  lmicsym  20979  nzerooringczr  21390  lmiclbs  21746  lmisfree  21751  lmictra  21754  mpfrcl  21992  ply1frcl  22205  pf1rcl  22236  mat1scmat  22426  toprntopon  22812  topnex  22883  neitr  23067  cmpsub  23287  bwth  23297  iunconn  23315  2ndcsb  23336  unisngl  23414  elpt  23459  ptclsg  23502  hmphsym  23669  hmphen  23672  haushmphlem  23674  cmphmph  23675  connhmph  23676  reghmph  23680  nrmhmph  23681  hmphdis  23683  indishmph  23685  hmphen2  23686  ufldom  23849  alexsubALTlem2  23935  alexsubALT  23938  metustfbas  24445  iunmbl2  25458  ioorcl2  25473  ioorinv2  25476  opnmblALT  25504  plyssc  26105  aannenlem2  26237  sslttr  27719  onscutlt  28165  istrkg2ld  28387  axcontlem4  28894  lfuhgr1v0e  29181  nbgr1vtx  29285  edgusgrnbfin  29300  cplgr1vlem  29356  cplgr1v  29357  fusgrn0degnn0  29427  g0wlk0  29580  wspthneq1eq2  29790  wlkswwlksf1o  29809  wwlksnndef  29835  wspthsnonn0vne  29847  eulerpath  30170  frgrwopreglem2  30242  friendship  30328  shintcli  31258  strlem1  32179  rexunirn  32421  iunrnmptss  32494  lsmsnorb  33362  mxidlnzrb  33451  prsdm  33904  prsrn  33905  0elsiga  34104  sigaclcu  34107  issgon  34113  insiga  34127  omssubaddlem  34290  omssubadd  34291  bnj906  34920  bnj938  34927  bnj1018g  34953  bnj1018  34954  bnj1020  34955  bnj1125  34982  bnj1145  34983  funen1cnv  35078  fineqvac  35087  onvf1odlem4  35093  lfuhgr3  35107  loop1cycl  35124  satfrnmapom  35357  satf0op  35364  sat1el2xp  35366  dmopab3rexdif  35392  mppspstlem  35558  txpss3v  35866  pprodss4v  35872  elsingles  35906  fnimage  35917  funpartlem  35930  funpartfun  35931  dfrdg4  35939  colinearex  36048  bj-cleljusti  36667  axc11n11r  36671  bj-exlimvmpi  36899  bj-snglex  36961  bj-unexg  37026  bj-bm1.3ii  37052  bj-restpw  37080  mptsnunlem  37326  ctbssinf  37394  pibt2  37405  wl-ax12v2cl  37494  wl-moteq  37502  wl-sbcom2d  37549  wl-mo3t  37564  ptrecube  37614  mblfinlem3  37653  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  indexdom  37728  xrnss3v  38354  prtlem16  38862  ricsym  42507  riccrng1  42509  ricdrng1  42516  sbccomieg  42781  setindtr  43013  setindtrs  43014  dfac11  43051  lnmlmic  43077  gicabl  43088  isnumbasgrplem1  43090  iscard4  43522  rtrclex  43606  clcnvlem  43612  brtrclfv2  43716  snhesn  43775  frege55b  43886  frege55c  43907  grucollcld  44249  grumnudlem  44274  iotain  44406  iotavalb  44419  sbiota1  44423  iunconnlem2  44924  permaxun  45001  permac8prim  45004  fnchoice  45023  stoweidlem59  46057  vitali2  46692  nsssmfmbf  46777  fsetprcnexALT  47063  funop1  47284  sbcpr  47522  gricen  47925  grlicsym  48005  grlictr  48007  grlicen  48009  gricgrlic  48010  usgrexmpl12ngric  48029  usgrexmpl12ngrlic  48030  opmpoismgm  48155  mo0sn  48804  mofmo  48835  mofeu  48836  f1mo  48841  eloprab1st2nd  48856  neircl  48893  sectrcl  49011  invrcl  49013  isorcl  49022  isoval2  49024  initc  49080  uobffth  49207  uobeqw  49208  fullthinc  49439  termco  49470  termcbasmo  49472  isinito3  49489  oppctermhom  49493  functermc  49497  termc2  49507  eufunclem  49510  eufunc  49511  euendfunc  49515  arweuthinc  49518  arweutermc  49519  discsntermlem  49559  rellan  49612  relran  49613  termolmd  49659  setrec1lem3  49678  elsetrecs  49689  elpglem1  49700