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 3140, 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 3140. 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  2537  mo3  2564  mo4  2566  moanimv  2619  euanv  2624  mopick  2625  clelab  2881  rexlimiva  3134  gencl  3507  cgsexg  3510  gencbvex2  3526  vtocleg  3537  vtoclgOLD  3555  eqvincg  3632  elrabi  3671  sbcex2  3831  sbccomlem  3849  eluni  4891  intab  4959  uniintsn  4966  dfiun2g  5011  disjiun  5112  trintss  5253  axrep6g  5265  sepexlem  5274  intex  5319  axpweq  5326  eunex  5365  eusvnf  5367  eusvnfb  5368  reusv2lem3  5375  unipw  5430  moabex  5439  nnullss  5442  exss  5443  sbcop1  5468  mosubopt  5490  opelopabsb  5510  relop  5835  dmopab2rex  5902  dmrnssfld  5958  dmsnopg  6207  unixp0  6277  elsnxp  6285  iotauni2  6505  iotanul2  6506  iotaex  6509  iotauni  6511  iota1  6513  iota4  6517  dffv2  6979  fveqdmss  7073  eldmrexrnb  7087  exfo  7100  funop  7144  funopdmsn  7145  funsndifnop  7146  csbriota  7382  eusvobj2  7402  fnoprabg  7535  limuni3  7852  tfindsg  7861  findsg  7898  elxp5  7924  f1oexbi  7929  ffoss  7949  fo1stres  8019  fo2ndres  8020  eloprabi  8067  frxp  8130  suppimacnv  8178  mpoxneldm  8216  mpoxopxnop0  8219  reldmtpos  8238  dftpos4  8249  frrlem2  8291  frrlem3  8292  frrlem4  8293  frrlem8  8297  wfrlem2OLD  8328  wfrlem3OLD  8329  wfrlem4OLD  8331  wfrdmclOLD  8336  wfrlem12OLD  8339  tfrlem9  8404  ecdmn0  8773  mapprc  8849  fsetprcnex  8881  ixpprc  8938  ixpn0  8949  bren  8974  brdomg  8976  brdomgOLD  8977  domssl  9017  domssr  9018  ener  9020  en0  9037  en0ALT  9038  en0r  9039  en1  9043  en1b  9044  2dom  9049  fiprc  9064  dom0  9121  pwdom  9148  domssex  9157  ssenen  9170  rexdif1enOLD  9178  dif1en  9179  dif1enOLD  9181  findcard2s  9184  ensymfib  9203  php  9226  phpOLD  9236  sdom1  9255  1sdom2dom  9260  isinf  9273  isinfOLD  9274  en1eqsn  9285  infn0  9317  pwfir  9332  fodomfir  9345  hartogslem1  9561  brwdom  9586  brwdomn0  9588  wdompwdom  9597  unxpwdom2  9607  ixpiunwdom  9609  infeq5  9656  brttrcl  9732  ttrcltr  9735  dmttrcl  9740  rnttrcl  9741  epfrs  9750  rankwflemb  9812  bnd2  9912  oncard  9979  carduni  10000  pm54.43  10020  ween  10054  acnrcl  10061  acndom  10070  acndom2  10073  iunfictbso  10133  aceq3lem  10139  dfac4  10141  dfac5lem4  10145  dfac5lem5  10146  dfac5lem4OLD  10147  dfac5  10148  dfac2a  10149  dfac2b  10150  dfacacn  10161  dfac12r  10166  kmlem2  10171  kmlem16  10185  ackbij2  10261  cff  10267  cardcf  10271  cfeq0  10275  cfsuc  10276  cff1  10277  cfcoflem  10291  coftr  10292  infpssr  10327  fin4en1  10328  isfin4-2  10333  enfin2i  10340  fin23lem21  10358  fin23lem30  10361  fin23lem41  10371  enfin1ai  10403  fin1a2lem7  10425  domtriomlem  10461  axdc2lem  10467  axdc3lem2  10470  axdc4lem  10474  axcclem  10476  ac6s  10503  zorn2lem7  10521  ttukey2g  10535  axdc  10540  brdom3  10547  brdom5  10548  brdom4  10549  brdom7disj  10550  brdom6disj  10551  konigthlem  10587  pwfseq  10683  tsk0  10782  gruina  10837  ltbtwnnq  10997  reclem2pr  11067  supsrlem  11130  supsr  11131  axpre-sup  11188  dedekindle  11404  nnunb  12502  ioorebas  13473  fzn0  13560  fzon0  13699  axdc4uzlem  14006  hasheqf1oi  14374  hash1snb  14442  hash1n0  14444  hashf1lem2  14479  hashle2pr  14500  hashge2el2difr  14504  hashge3el3dif  14510  fi1uzind  14530  brfi1indALT  14533  swrdcl  14668  pfxcl  14700  relexpindlem  15087  fclim  15574  climmo  15578  rlimdmo1  15639  cicsym  17822  cictr  17823  brssc  17832  sscpwex  17833  initoid  18019  termoid  18020  initoeu1  18029  initoeu2lem1  18032  initoeu2  18034  termoeu1  18036  opifismgm  18642  grpidval  18644  dfgrp3e  19028  subgint  19138  giclcl  19261  gicrcl  19262  gicsym  19263  gicen  19266  gicsubgen  19267  cntzssv  19316  symgvalstruct  19383  giccyg  19886  brric2  20471  ricgic  20472  subrngint  20525  subrgint  20560  abvn0b  20801  lmiclcl  21033  lmicrcl  21034  lmicsym  21035  nzerooringczr  21446  lmiclbs  21802  lmisfree  21807  lmictra  21810  mpfrcl  22048  ply1frcl  22261  pf1rcl  22292  mat1scmat  22482  toprntopon  22868  topnex  22939  neitr  23123  cmpsub  23343  bwth  23353  iunconn  23371  2ndcsb  23392  unisngl  23470  elpt  23515  ptclsg  23558  hmphsym  23725  hmphen  23728  haushmphlem  23730  cmphmph  23731  connhmph  23732  reghmph  23736  nrmhmph  23737  hmphdis  23739  indishmph  23741  hmphen2  23742  ufldom  23905  alexsubALTlem2  23991  alexsubALT  23994  metustfbas  24501  iunmbl2  25515  ioorcl2  25530  ioorinv2  25533  opnmblALT  25561  plyssc  26162  aannenlem2  26294  sslttr  27776  onscutlt  28222  istrkg2ld  28444  axcontlem4  28951  lfuhgr1v0e  29238  nbgr1vtx  29342  edgusgrnbfin  29357  cplgr1vlem  29413  cplgr1v  29414  fusgrn0degnn0  29484  g0wlk0  29637  wspthneq1eq2  29847  wlkswwlksf1o  29866  wwlksnndef  29892  wspthsnonn0vne  29904  eulerpath  30227  frgrwopreglem2  30299  friendship  30385  shintcli  31315  strlem1  32236  rexunirn  32478  iunrnmptss  32551  lsmsnorb  33411  mxidlnzrb  33500  prsdm  33950  prsrn  33951  0elsiga  34150  sigaclcu  34153  issgon  34159  insiga  34173  omssubaddlem  34336  omssubadd  34337  bnj906  34966  bnj938  34973  bnj1018g  34999  bnj1018  35000  bnj1020  35001  bnj1125  35028  bnj1145  35029  funen1cnv  35124  fineqvac  35133  lfuhgr3  35147  loop1cycl  35164  satfrnmapom  35397  satf0op  35404  sat1el2xp  35406  dmopab3rexdif  35432  mppspstlem  35598  txpss3v  35901  pprodss4v  35907  elsingles  35941  fnimage  35952  funpartlem  35965  funpartfun  35966  dfrdg4  35974  colinearex  36083  bj-cleljusti  36702  axc11n11r  36706  bj-exlimvmpi  36934  bj-snglex  36996  bj-unexg  37061  bj-bm1.3ii  37087  bj-restpw  37115  mptsnunlem  37361  ctbssinf  37429  pibt2  37440  wl-ax12v2cl  37529  wl-moteq  37537  wl-sbcom2d  37584  wl-mo3t  37599  ptrecube  37649  mblfinlem3  37688  ovoliunnfl  37691  voliunnfl  37693  volsupnfl  37694  indexdom  37763  xrnss3v  38395  prtlem16  38892  ricsym  42517  riccrng1  42519  ricdrng1  42526  sbccomieg  42791  setindtr  43023  setindtrs  43024  dfac11  43061  lnmlmic  43087  gicabl  43098  isnumbasgrplem1  43100  iscard4  43532  rtrclex  43616  clcnvlem  43622  brtrclfv2  43726  snhesn  43785  frege55b  43896  frege55c  43917  grucollcld  44259  grumnudlem  44284  iotain  44416  iotavalb  44429  sbiota1  44433  iunconnlem2  44934  permaxun  45011  permac8prim  45014  fnchoice  45033  stoweidlem59  46068  vitali2  46703  nsssmfmbf  46788  fsetprcnexALT  47071  funop1  47292  sbcpr  47515  gricen  47918  grlicsym  47998  grlictr  48000  grlicen  48002  gricgrlic  48003  usgrexmpl12ngric  48022  usgrexmpl12ngrlic  48023  opmpoismgm  48122  mo0sn  48774  mofmo  48805  mofeu  48806  f1mo  48811  eloprab1st2nd  48823  neircl  48859  fullthinc  49316  termcbasmo  49348  isinito3  49365  oppctermhom  49369  functermc  49373  termc2  49383  eufunclem  49386  eufunc  49387  euendfunc  49391  arweuthinc  49394  arweutermc  49395  discsntermlem  49427  rellan  49478  relran  49479  setrec1lem3  49533  elsetrecs  49544  elpglem1  49555