Theorem exlimiv 1932

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

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

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  exlimiiv  1933  exlimivv  1934  exsbim  2004  ax8  2120  ax9  2128  dfeumo  2537  mo3  2565  mo4  2567  moanimv  2620  euanv  2625  mopick  2626  clelab  2881  rexlimiva  3131  gencl  3484  cgsexg  3487  gencbvex2  3502  vtocleg  3512  eqvincg  3604  elrabi  3644  sbcex2  3803  sbccomlem  3821  eluni  4868  intab  4935  uniintsn  4942  dfiun2g  4987  disjiun  5088  trintss  5225  axrep6g  5237  sepexlem  5246  intex  5291  axpweq  5298  eunex  5337  eusvnf  5339  eusvnfb  5340  reusv2lem3  5347  axprglem  5382  axprg  5383  unipw  5405  moabex  5413  moabexOLD  5414  nnullss  5417  exss  5418  sbcop1  5444  mosubopt  5466  opelopabsb  5486  relop  5807  dmopab2rex  5874  dmrnssfld  5931  dmsnopg  6179  unixp0  6249  elsnxp  6257  iotauni2  6472  iotanul2  6473  iotaex  6476  iotauni  6477  iota1  6479  iota4  6481  dffv2  6937  fveqdmss  7032  eldmrexrnb  7046  exfo  7059  funop  7104  funopdmsn  7105  funsndifnop  7106  csbriota  7340  eusvobj2  7360  fnoprabg  7491  limuni3  7804  tfindsg  7813  findsg  7849  elxp5  7875  f1oexbi  7880  ffoss  7900  fo1stres  7969  fo2ndres  7970  eloprabi  8017  frxp  8078  suppimacnv  8126  mpoxneldm  8164  mpoxopxnop0  8167  reldmtpos  8186  dftpos4  8197  frrlem2  8239  frrlem3  8240  frrlem4  8241  frrlem8  8245  tfrlem9  8326  ecdmn0  8698  mapprc  8779  fsetprcnex  8811  ixpprc  8869  ixpn0  8880  bren  8905  brdomg  8907  domssl  8947  domssr  8948  ener  8950  en0  8967  en0ALT  8968  en0r  8969  en1  8973  en1b  8974  2dom  8979  fiprc  8993  dom0  9045  pwdom  9069  domssex  9078  ssenen  9091  dif1en  9098  findcard2s  9102  ensymfib  9120  php  9143  sdom1  9162  1sdom2dom  9166  isinf  9177  en1eqsn  9187  infn0  9214  pwfir  9229  fodomfir  9240  hartogslem1  9459  brwdom  9484  brwdomn0  9486  wdompwdom  9495  unxpwdom2  9505  ixpiunwdom  9507  elirrv  9514  infeq5  9558  brttrcl  9634  ttrcltr  9637  dmttrcl  9642  rnttrcl  9643  epfrs  9652  rankwflemb  9717  bnd2  9817  oncard  9884  carduni  9905  pm54.43  9925  ween  9957  acnrcl  9964  acndom  9973  acndom2  9976  iunfictbso  10036  aceq3lem  10042  dfac4  10044  dfac5lem4  10048  dfac5lem5  10049  dfac5lem4OLD  10050  dfac5  10051  dfac2a  10052  dfac2b  10053  dfacacn  10064  dfac12r  10069  kmlem2  10074  kmlem16  10088  ackbij2  10164  cff  10170  cardcf  10174  cfeq0  10178  cfsuc  10179  cff1  10180  cfcoflem  10194  coftr  10195  infpssr  10230  fin4en1  10231  isfin4-2  10236  enfin2i  10243  fin23lem21  10261  fin23lem30  10264  fin23lem41  10274  enfin1ai  10306  fin1a2lem7  10328  domtriomlem  10364  axdc2lem  10370  axdc3lem2  10373  axdc4lem  10377  axcclem  10379  ac6s  10406  zorn2lem7  10424  ttukey2g  10438  axdc  10443  brdom3  10450  brdom5  10451  brdom4  10452  brdom7disj  10453  brdom6disj  10454  konigthlem  10491  pwfseq  10587  tsk0  10686  gruina  10741  ltbtwnnq  10901  reclem2pr  10971  supsrlem  11034  supsr  11035  axpre-sup  11092  dedekindle  11309  nnunb  12409  ioorebas  13379  fzn0  13466  fzon0  13605  axdc4uzlem  13918  hasheqf1oi  14286  hash1snb  14354  hash1n0  14356  hashf1lem2  14391  hashle2pr  14412  hashge2el2difr  14416  hashge3el3dif  14422  fi1uzind  14442  brfi1indALT  14445  swrdcl  14581  pfxcl  14613  relexpindlem  14998  fclim  15488  climmo  15492  rlimdmo1  15553  cicsym  17740  cictr  17741  brssc  17750  sscpwex  17751  initoid  17937  termoid  17938  initoeu1  17947  initoeu2lem1  17950  initoeu2  17952  termoeu1  17954  opifismgm  18596  grpidval  18598  dfgrp3e  18982  subgint  19092  giclcl  19214  gicrcl  19215  gicsym  19216  gicen  19219  gicsubgen  19220  cntzssv  19269  symgvalstruct  19338  giccyg  19841  brric2  20451  ricgic  20452  subrngint  20505  subrgint  20540  abvn0b  20781  lmiclcl  21034  lmicrcl  21035  lmicsym  21036  nzerooringczr  21447  lmiclbs  21804  lmisfree  21809  lmictra  21812  mpfrcl  22052  ply1frcl  22274  pf1rcl  22305  mat1scmat  22495  toprntopon  22881  topnex  22952  neitr  23136  cmpsub  23356  bwth  23366  iunconn  23384  2ndcsb  23405  unisngl  23483  elpt  23528  ptclsg  23571  hmphsym  23738  hmphen  23741  haushmphlem  23743  cmphmph  23744  connhmph  23745  reghmph  23749  nrmhmph  23750  hmphdis  23752  indishmph  23754  hmphen2  23755  ufldom  23918  alexsubALTlem2  24004  alexsubALT  24007  metustfbas  24513  iunmbl2  25526  ioorcl2  25541  ioorinv2  25544  opnmblALT  25572  plyssc  26173  aannenlem2  26305  sltstr  27795  oncutlt  28272  istrkg2ld  28544  axcontlem4  29052  lfuhgr1v0e  29339  nbgr1vtx  29443  edgusgrnbfin  29458  cplgr1vlem  29514  cplgr1v  29515  fusgrn0degnn0  29585  g0wlk0  29736  wspthneq1eq2  29945  wlkswwlksf1o  29964  wwlksnndef  29990  wspthsnonn0vne  30002  eulerpath  30328  frgrwopreglem2  30400  friendship  30486  shintcli  31417  strlem1  32338  rexunirn  32578  iunrnmptss  32652  lsmsnorb  33484  mxidlnzrb  33573  prsdm  34092  prsrn  34093  0elsiga  34292  sigaclcu  34295  issgon  34301  insiga  34315  omssubaddlem  34477  omssubadd  34478  bnj906  35106  bnj938  35113  bnj1018g  35139  bnj1018  35140  bnj1020  35141  bnj1125  35168  bnj1145  35169  funen1cnv  35265  axprALT2  35287  fineqvac  35294  fineqvnttrclselem1  35299  fineqvnttrclselem2  35300  onvf1odlem4  35322  lfuhgr3  35336  loop1cycl  35353  satfrnmapom  35586  satf0op  35593  sat1el2xp  35595  dmopab3rexdif  35621  mppspstlem  35787  txpss3v  36092  pprodss4v  36098  elsingles  36132  fnimage  36143  funpartlem  36158  funpartfun  36159  dfrdg4  36167  colinearex  36276  regsfromregtr  36690  bj-cleljusti  36924  axc11n11r  36928  bj-exlimvmpi  37159  bj-snglex  37221  bj-unexg  37286  bj-bm1.3ii  37312  bj-axseprep  37322  bj-restpw  37345  mptsnunlem  37593  ctbssinf  37661  pibt2  37672  wl-ax12v2cl  37761  wl-moteq  37769  wl-sbcom2d  37816  wl-mo3t  37831  ptrecube  37871  mblfinlem3  37910  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  indexdom  37985  xrnss3v  38632  prtlem16  39245  ricsym  42889  riccrng1  42891  ricdrng1  42898  sbccomieg  43150  setindtr  43381  setindtrs  43382  dfac11  43419  lnmlmic  43445  gicabl  43456  isnumbasgrplem1  43458  iscard4  43889  rtrclex  43973  clcnvlem  43979  brtrclfv2  44083  snhesn  44142  frege55b  44253  frege55c  44274  grucollcld  44616  grumnudlem  44641  iotain  44773  iotavalb  44786  sbiota1  44790  iunconnlem2  45290  permaxun  45367  permac8prim  45370  fnchoice  45389  stoweidlem59  46417  vitali2  47052  nsssmfmbf  47137  fsetprcnexALT  47422  funop1  47643  sbcpr  47881  gricen  48285  grlicsym  48373  grlictr  48375  grlicen  48377  gricgrlic  48378  usgrexmpl12ngric  48398  usgrexmpl12ngrlic  48399  opmpoismgm  48527  mo0sn  49175  mofmo  49206  mofeu  49207  f1mo  49212  eloprab1st2nd  49227  neircl  49264  sectrcl  49381  invrcl  49383  isorcl  49392  isoval2  49394  initc  49450  uobffth  49577  uobeqw  49578  fullthinc  49809  termco  49840  termcbasmo  49842  isinito3  49859  oppctermhom  49863  functermc  49867  termc2  49877  eufunclem  49880  eufunc  49881  euendfunc  49885  arweuthinc  49888  arweutermc  49889  discsntermlem  49929  rellan  49982  relran  49983  termolmd  50029  setrec1lem3  50048  elsetrecs  50059  elpglem1  50070