Theorem exlimiv 1933

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

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

This inference, along with its many variants such as rexlimdv 3153, 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 3153. 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 1933 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1934. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1971 and ax-8 2108. (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 1915	. 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 1913

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

This theorem is referenced by:  exlimiiv  1934  exlimivv  1935  exsbim  2005  ax8  2112  ax9  2120  dfeumo  2531  mo3  2558  mo4  2560  moanimv  2615  euanv  2620  mopick  2621  clelab  2879  rexlimiva  3147  gencl  3515  cgsexg  3518  ceqsexvOLD  3526  gencbvex2  3536  vtocleg  3545  vtoclgOLD  3557  eqvincg  3635  elrabi  3676  elrabiOLD  3677  sbcex2  3841  eluni  4910  intab  4981  uniintsn  4990  dfiun2g  5032  disjiun  5134  trintss  5283  axrep6g  5292  intex  5336  axpweq  5347  eunex  5387  eusvnf  5389  eusvnfb  5390  reusv2lem3  5397  unipw  5449  moabex  5458  nnullss  5461  exss  5462  sbcop1  5487  mosubopt  5509  opelopabsb  5529  relop  5848  dmopab2rex  5915  dmrnssfld  5967  dmsnopg  6209  unixp0  6279  elsnxp  6287  iotauni2  6509  iotanul2  6510  iotaex  6513  iotauni  6515  iota1  6517  iota4  6521  dffv2  6983  fveqdmss  7077  eldmrexrnb  7090  exfo  7103  funop  7143  funopdmsn  7144  funsndifnop  7145  csbriota  7377  eusvobj2  7397  fnoprabg  7527  limuni3  7837  tfindsg  7846  findsg  7886  elxp5  7910  f1oexbi  7915  ffoss  7928  fo1stres  7997  fo2ndres  7998  eloprabi  8045  frxp  8108  suppimacnv  8155  mpoxneldm  8193  mpoxopxnop0  8196  reldmtpos  8215  dftpos4  8226  frrlem2  8268  frrlem3  8269  frrlem4  8270  frrlem8  8274  wfrlem2OLD  8305  wfrlem3OLD  8306  wfrlem4OLD  8308  wfrdmclOLD  8313  wfrlem12OLD  8316  tfrlem9  8381  ecdmn0  8746  mapprc  8820  fsetprcnex  8852  ixpprc  8909  ixpn0  8920  bren  8945  brenOLD  8946  brdomg  8948  brdomgOLD  8949  domssl  8990  domssr  8991  ener  8993  en0  9009  en0OLD  9010  en0ALT  9011  en0r  9012  en1  9017  en1OLD  9018  en1b  9019  en1bOLD  9020  2dom  9026  fiprc  9041  dom0  9098  pwdom  9125  domssex  9134  ssenen  9147  rexdif1enOLD  9155  dif1en  9156  dif1enOLD  9158  findcard2s  9161  pwfir  9172  ensymfib  9183  php  9206  phpOLD  9218  sdom1  9238  1sdom2dom  9243  isinf  9256  isinfOLD  9257  en1eqsn  9270  infn0  9303  hartogslem1  9533  brwdom  9558  brwdomn0  9560  wdompwdom  9569  unxpwdom2  9579  ixpiunwdom  9581  infeq5  9628  omex  9634  brttrcl  9704  ttrcltr  9707  dmttrcl  9712  rnttrcl  9713  epfrs  9722  rankwflemb  9784  bnd2  9884  oncard  9951  carduni  9972  pm54.43  9992  ween  10026  acnrcl  10033  acndom  10042  acndom2  10045  iunfictbso  10105  aceq3lem  10111  dfac4  10113  dfac5lem4  10117  dfac5lem5  10118  dfac5  10119  dfac2a  10120  dfac2b  10121  dfacacn  10132  dfac12r  10137  kmlem2  10142  kmlem16  10156  ackbij2  10234  cff  10239  cardcf  10243  cfeq0  10247  cfsuc  10248  cff1  10249  cfcoflem  10263  coftr  10264  infpssr  10299  fin4en1  10300  isfin4-2  10305  enfin2i  10312  fin23lem21  10330  fin23lem30  10333  fin23lem41  10343  enfin1ai  10375  fin1a2lem7  10397  domtriomlem  10433  axdc2lem  10439  axdc3lem2  10442  axdc4lem  10446  axcclem  10448  ac6s  10475  zorn2lem7  10493  ttukey2g  10507  axdc  10512  brdom3  10519  brdom5  10520  brdom4  10521  brdom7disj  10522  brdom6disj  10523  konigthlem  10559  pwcfsdom  10574  pwfseq  10655  tsk0  10754  gruina  10809  ltbtwnnq  10969  reclem2pr  11039  supsrlem  11102  supsr  11103  axpre-sup  11160  dedekindle  11374  nnunb  12464  ioorebas  13424  fzn0  13511  fzon0  13646  axdc4uzlem  13944  hasheqf1oi  14307  hash1snb  14375  hash1n0  14377  hashf1lem2  14413  hashle2pr  14434  hashge2el2difr  14438  hashge3el3dif  14443  fi1uzind  14454  brfi1indALT  14457  swrdcl  14591  pfxcl  14623  relexpindlem  15006  fclim  15493  climmo  15497  rlimdmo1  15558  cicsym  17747  cictr  17748  brssc  17757  sscpwex  17758  initoid  17947  termoid  17948  initoeu1  17957  initoeu2lem1  17960  initoeu2  17962  termoeu1  17964  opifismgm  18574  grpidval  18576  dfgrp3e  18919  subgint  19024  giclcl  19140  gicrcl  19141  gicsym  19142  gicen  19145  gicsubgen  19146  cntzssv  19186  symgvalstruct  19258  symgvalstructOLD  19259  giccyg  19762  brric2  20277  ricgic  20278  subrgint  20378  lmiclcl  20673  lmicrcl  20674  lmicsym  20675  abvn0b  20912  lmiclbs  21383  lmisfree  21388  lmictra  21391  mpfrcl  21639  ply1frcl  21828  pf1rcl  21859  mat1scmat  22032  toprntopon  22418  topnex  22490  neitr  22675  cmpsub  22895  bwth  22905  iunconn  22923  2ndcsb  22944  unisngl  23022  elpt  23067  ptclsg  23110  hmphsym  23277  hmphen  23280  haushmphlem  23282  cmphmph  23283  connhmph  23284  reghmph  23288  nrmhmph  23289  hmphdis  23291  indishmph  23293  hmphen2  23294  ufldom  23457  alexsubALTlem2  23543  alexsubALT  23546  metustfbas  24057  iunmbl2  25065  ioorcl2  25080  ioorinv2  25083  opnmblALT  25111  plyssc  25705  aannenlem2  25833  mulog2sum  27029  sslttr  27297  istrkg2ld  27700  axcontlem4  28214  lfuhgr1v0e  28500  nbgr1vtx  28604  edgusgrnbfin  28619  cplgr1vlem  28675  cplgr1v  28676  fusgrn0degnn0  28745  g0wlk0  28898  wspthneq1eq2  29103  wlkswwlksf1o  29122  wwlksnndef  29148  wspthsnonn0vne  29160  eulerpath  29483  frgrwopreglem2  29555  friendship  29641  shintcli  30569  strlem1  31490  rexunirn  31719  iunrnmptss  31784  cnvoprabOLD  31932  lsmsnorb  32489  mxidlnzrb  32583  prsdm  32882  prsrn  32883  0elsiga  33100  sigaclcu  33103  issgon  33109  insiga  33123  omssubaddlem  33286  omssubadd  33287  bnj906  33929  bnj938  33936  bnj1018g  33962  bnj1018  33963  bnj1020  33964  bnj1125  33991  bnj1145  33992  funen1cnv  34079  fineqvac  34085  lfuhgr3  34098  loop1cycl  34116  satfrnmapom  34349  satf0op  34356  sat1el2xp  34358  dmopab3rexdif  34384  mppspstlem  34550  txpss3v  34838  pprodss4v  34844  elsingles  34878  fnimage  34889  funpartlem  34902  funpartfun  34903  dfrdg4  34911  colinearex  35020  bj-cleljusti  35545  axc11n11r  35549  bj-exlimvmpi  35779  bj-snglex  35842  bj-unexg  35907  bj-bm1.3ii  35933  bj-restpw  35961  mptsnunlem  36207  ctbssinf  36275  pibt2  36286  wl-moteq  36371  wl-sbcom2d  36414  wl-mo3t  36429  ptrecube  36476  mblfinlem3  36515  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  indexdom  36590  xrnss3v  37230  prtlem16  37727  ricsym  41091  riccrng1  41093  ricdrng1  41099  sbccomieg  41516  setindtr  41748  setindtrs  41749  dfac11  41789  lnmlmic  41815  gicabl  41826  isnumbasgrplem1  41828  iscard4  42269  rtrclex  42353  clcnvlem  42359  brtrclfv2  42463  snhesn  42522  frege55b  42633  frege55c  42654  grucollcld  43004  grumnudlem  43029  iotain  43161  iotavalb  43174  sbiota1  43178  iunconnlem2  43681  fnchoice  43698  stoweidlem59  44761  vitali2  45396  nsssmfmbf  45481  fsetprcnexALT  45758  funop1  45977  sbcpr  46175  opmpoismgm  46563  subrngint  46723  nzerooringczr  46923  mo0sn  47453  mofmo  47466  mofeu  47467  f1mo  47472  neircl  47490  fullthinc  47619  setrec1lem3  47687  elsetrecs  47698  elpglem1  47709