Theorem exlimiv 1934

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

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

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

Syntax hints:   → wi 4  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

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

This theorem is referenced by:  exlimiiv  1935  exlimivv  1936  exsbim  2006  ax8  2114  ax9  2122  dfeumo  2537  mo3  2564  mo4  2566  moanimv  2621  euanv  2626  mopick  2627  clelab  2882  gencl  3461  cgsexg  3464  ceqsexv  3469  gencbvex2  3479  vtoclg  3495  vtocleg  3511  eqvincg  3570  elrabi  3611  elrabiOLD  3612  sbcex2  3777  eluni  4839  intab  4906  uniintsn  4915  disjiun  5057  trintss  5204  intex  5256  axpweq  5282  eunex  5308  eusvnf  5310  eusvnfb  5311  reusv2lem3  5318  unipw  5360  moabex  5368  nnullss  5371  exss  5372  sbcop1  5396  mosubopt  5418  opelopabsb  5436  relop  5748  dmopab2rex  5815  dmrnssfld  5868  dmsnopg  6105  unixp0  6175  elsnxp  6183  iotauni  6393  iota1  6395  iota4  6399  dffv2  6845  fveqdmss  6938  eldmrexrnb  6950  exfo  6963  funop  7003  funopdmsn  7004  funsndifnop  7005  csbriota  7228  eusvobj2  7248  fnoprabg  7375  limuni3  7674  tfindsg  7682  findsg  7720  elxp5  7744  f1oexbi  7749  ffoss  7762  fo1stres  7830  fo2ndres  7831  eloprabi  7876  frxp  7938  suppimacnv  7961  mpoxneldm  7999  mpoxopxnop0  8002  reldmtpos  8021  dftpos4  8032  frrlem2  8074  frrlem3  8075  frrlem4  8076  frrlem8  8080  wfrlem2OLD  8111  wfrlem3OLD  8112  wfrlem4OLD  8114  wfrdmclOLD  8119  wfrlem12OLD  8122  tfrlem9  8187  ecdmn0  8503  mapprc  8577  fsetprcnex  8608  ixpprc  8665  ixpn0  8676  bren  8701  brenOLD  8702  brdomg  8703  ener  8742  en0  8758  en0OLD  8759  en0ALT  8760  en1  8765  en1OLD  8766  en1b  8767  en1bOLD  8768  2dom  8774  fiprc  8789  pwdom  8865  domssex  8874  ssenen  8887  php  8897  rexdif1en  8906  dif1en  8907  findcard2s  8910  pwfir  8921  ensymfib  8930  isinf  8965  hartogslem1  9231  brwdom  9256  brwdomn0  9258  wdompwdom  9267  unxpwdom2  9277  ixpiunwdom  9279  infeq5  9325  omex  9331  epfrs  9420  rankwflemb  9482  bnd2  9582  oncard  9649  carduni  9670  pm54.43  9690  ween  9722  acnrcl  9729  acndom  9738  acndom2  9741  iunfictbso  9801  aceq3lem  9807  dfac4  9809  dfac5lem4  9813  dfac5lem5  9814  dfac5  9815  dfac2a  9816  dfac2b  9817  dfacacn  9828  dfac12r  9833  kmlem2  9838  kmlem16  9852  ackbij2  9930  cff  9935  cardcf  9939  cfeq0  9943  cfsuc  9944  cff1  9945  cfcoflem  9959  coftr  9960  infpssr  9995  fin4en1  9996  isfin4-2  10001  enfin2i  10008  fin23lem21  10026  fin23lem30  10029  fin23lem41  10039  enfin1ai  10071  fin1a2lem7  10093  domtriomlem  10129  axdc2lem  10135  axdc3lem2  10138  axdc4lem  10142  axcclem  10144  ac6s  10171  zorn2lem7  10189  ttukey2g  10203  axdc  10208  brdom3  10215  brdom5  10216  brdom4  10217  brdom7disj  10218  brdom6disj  10219  konigthlem  10255  pwcfsdom  10270  pwfseq  10351  tsk0  10450  gruina  10505  ltbtwnnq  10665  reclem2pr  10735  supsrlem  10798  supsr  10799  axpre-sup  10856  dedekindle  11069  nnunb  12159  ioorebas  13112  fzn0  13199  fzon0  13333  axdc4uzlem  13631  hasheqf1oi  13994  hash1snb  14062  hash1n0  14064  hashf1lem2  14098  hashle2pr  14119  hashge2el2difr  14123  hashge3el3dif  14128  fi1uzind  14139  brfi1indALT  14142  swrdcl  14286  pfxcl  14318  relexpindlem  14702  fclim  15190  climmo  15194  rlimdmo1  15255  cicsym  17433  cictr  17434  brssc  17443  sscpwex  17444  initoid  17632  termoid  17633  initoeu1  17642  initoeu2lem1  17645  initoeu2  17647  termoeu1  17649  opifismgm  18258  grpidval  18260  dfgrp3e  18590  subgint  18694  giclcl  18803  gicrcl  18804  gicsym  18805  gicen  18808  gicsubgen  18809  cntzssv  18849  symgvalstruct  18919  symgvalstructOLD  18920  giccyg  19416  brric2  19904  ricgic  19905  subrgint  19961  lmiclcl  20247  lmicrcl  20248  lmicsym  20249  abvn0b  20486  lmiclbs  20954  lmisfree  20959  lmictra  20962  mpfrcl  21205  ply1frcl  21394  pf1rcl  21425  mat1scmat  21596  toprntopon  21982  topnex  22054  neitr  22239  cmpsub  22459  bwth  22469  iunconn  22487  2ndcsb  22508  unisngl  22586  elpt  22631  ptclsg  22674  hmphsym  22841  hmphen  22844  haushmphlem  22846  cmphmph  22847  connhmph  22848  reghmph  22852  nrmhmph  22853  hmphdis  22855  indishmph  22857  hmphen2  22858  ufldom  23021  alexsubALTlem2  23107  alexsubALT  23110  metustfbas  23619  iunmbl2  24626  ioorcl2  24641  ioorinv2  24644  opnmblALT  24672  plyssc  25266  aannenlem2  25394  mulog2sum  26590  istrkg2ld  26725  axcontlem4  27238  lfuhgr1v0e  27524  nbgr1vtx  27628  edgusgrnbfin  27643  cplgr1vlem  27699  cplgr1v  27700  fusgrn0degnn0  27769  g0wlk0  27921  wspthneq1eq2  28126  wlkswwlksf1o  28145  wwlksnndef  28171  wspthsnonn0vne  28183  eulerpath  28506  frgrwopreglem2  28578  friendship  28664  shintcli  29592  strlem1  30513  rexunirn  30741  iunrnmptss  30806  cnvoprabOLD  30957  lsmsnorb  31481  mxidlnzrb  31546  prsdm  31766  prsrn  31767  0elsiga  31982  sigaclcu  31985  issgon  31991  insiga  32005  omssubaddlem  32166  omssubadd  32167  bnj521  32616  bnj906  32810  bnj938  32817  bnj1018g  32843  bnj1018  32844  bnj1020  32845  bnj1125  32872  bnj1145  32873  funen1cnv  32960  fineqvac  32966  lfuhgr3  32981  loop1cycl  32999  satfrnmapom  33232  satf0op  33239  sat1el2xp  33241  dmopab3rexdif  33267  mppspstlem  33433  brttrcl  33699  ttrcltr  33702  dmttrcl  33707  rnttrcl  33708  sslttr  33928  txpss3v  34107  pprodss4v  34113  elsingles  34147  fnimage  34158  funpartlem  34171  funpartfun  34172  dfrdg4  34180  colinearex  34289  bj-cleljusti  34788  axc11n11r  34792  bj-exlimvmpi  35023  bj-snglex  35090  bj-bm1.3ii  35162  bj-restpw  35190  mptsnunlem  35436  ctbssinf  35504  pibt2  35515  wl-moteq  35600  wl-sbcom2d  35643  wl-mo3t  35658  ptrecube  35704  mblfinlem3  35743  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  indexdom  35819  xrnss3v  36429  prtlem16  36810  sn-iotauni  40120  sn-iotanul  40121  sn-iotaex  40123  sbccomieg  40531  setindtr  40762  setindtrs  40763  dfac11  40803  lnmlmic  40829  gicabl  40840  isnumbasgrplem1  40842  iscard4  41038  rtrclex  41114  clcnvlem  41120  brtrclfv2  41224  snhesn  41283  frege55b  41394  frege55c  41415  grucollcld  41767  grumnudlem  41792  iotain  41924  iotavalb  41937  sbiota1  41941  iunconnlem2  42444  fnchoice  42461  stoweidlem59  43490  vitali2  44122  nsssmfmbf  44201  fsetprcnexALT  44443  funop1  44662  sbcpr  44861  opmpoismgm  45249  nzerooringczr  45518  mo0sn  46049  mofmo  46062  mofeu  46063  f1mo  46068  neircl  46086  fullthinc  46215  setrec1lem3  46281  elsetrecs  46291  elpglem1  46302