Theorem exlimiv 1934

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

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

This inference, along with its many variants such as rexlimdv 3213, 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 3213. 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 2109. (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 1782

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

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

This theorem is referenced by:  exlimiiv  1935  exlimivv  1936  exsbim  2006  ax8  2113  ax9  2121  dfeumo  2538  mo3  2565  mo4  2567  moanimv  2622  euanv  2627  mopick  2628  clelab  2884  gencl  3472  cgsexg  3475  ceqsexv  3480  gencbvex2  3490  vtoclg  3506  vtocleg  3522  eqvincg  3579  elrabi  3619  elrabiOLD  3620  sbcex2  3782  eluni  4843  intab  4910  uniintsn  4919  dfiun2g  4961  disjiun  5062  trintss  5209  axrep6g  5218  intex  5262  axpweq  5288  eunex  5314  eusvnf  5316  eusvnfb  5317  reusv2lem3  5324  unipw  5367  moabex  5375  nnullss  5378  exss  5379  sbcop1  5403  mosubopt  5425  opelopabsb  5444  relop  5762  dmopab2rex  5829  dmrnssfld  5882  dmsnopg  6121  unixp0  6190  elsnxp  6198  iotauni  6412  iota1  6414  iota4  6418  dffv2  6872  fveqdmss  6965  eldmrexrnb  6977  exfo  6990  funop  7030  funopdmsn  7031  funsndifnop  7032  csbriota  7257  eusvobj2  7277  fnoprabg  7406  limuni3  7708  tfindsg  7716  findsg  7755  elxp5  7779  f1oexbi  7784  ffoss  7797  fo1stres  7866  fo2ndres  7867  eloprabi  7912  frxp  7976  suppimacnv  7999  mpoxneldm  8037  mpoxopxnop0  8040  reldmtpos  8059  dftpos4  8070  frrlem2  8112  frrlem3  8113  frrlem4  8114  frrlem8  8118  wfrlem2OLD  8149  wfrlem3OLD  8150  wfrlem4OLD  8152  wfrdmclOLD  8157  wfrlem12OLD  8160  tfrlem9  8225  ecdmn0  8554  mapprc  8628  fsetprcnex  8659  ixpprc  8716  ixpn0  8727  bren  8752  brenOLD  8753  brdomg  8755  brdomgOLD  8756  ener  8796  en0  8812  en0OLD  8813  en0ALT  8814  en0r  8815  en1  8820  en1OLD  8821  en1b  8822  en1bOLD  8823  2dom  8829  fiprc  8844  dom0  8898  pwdom  8925  domssex  8934  ssenen  8947  rexdif1en  8953  dif1en  8954  findcard2s  8957  pwfir  8968  ensymfib  8979  php  9002  phpOLD  9014  isinf  9045  hartogslem1  9310  brwdom  9335  brwdomn0  9337  wdompwdom  9346  unxpwdom2  9356  ixpiunwdom  9358  infeq5  9404  omex  9410  brttrcl  9480  ttrcltr  9483  dmttrcl  9488  rnttrcl  9489  epfrs  9498  rankwflemb  9560  bnd2  9660  oncard  9727  carduni  9748  pm54.43  9768  ween  9800  acnrcl  9807  acndom  9816  acndom2  9819  iunfictbso  9879  aceq3lem  9885  dfac4  9887  dfac5lem4  9891  dfac5lem5  9892  dfac5  9893  dfac2a  9894  dfac2b  9895  dfacacn  9906  dfac12r  9911  kmlem2  9916  kmlem16  9930  ackbij2  10008  cff  10013  cardcf  10017  cfeq0  10021  cfsuc  10022  cff1  10023  cfcoflem  10037  coftr  10038  infpssr  10073  fin4en1  10074  isfin4-2  10079  enfin2i  10086  fin23lem21  10104  fin23lem30  10107  fin23lem41  10117  enfin1ai  10149  fin1a2lem7  10171  domtriomlem  10207  axdc2lem  10213  axdc3lem2  10216  axdc4lem  10220  axcclem  10222  ac6s  10249  zorn2lem7  10267  ttukey2g  10281  axdc  10286  brdom3  10293  brdom5  10294  brdom4  10295  brdom7disj  10296  brdom6disj  10297  konigthlem  10333  pwcfsdom  10348  pwfseq  10429  tsk0  10528  gruina  10583  ltbtwnnq  10743  reclem2pr  10813  supsrlem  10876  supsr  10877  axpre-sup  10934  dedekindle  11148  nnunb  12238  ioorebas  13192  fzn0  13279  fzon0  13414  axdc4uzlem  13712  hasheqf1oi  14075  hash1snb  14143  hash1n0  14145  hashf1lem2  14179  hashle2pr  14200  hashge2el2difr  14204  hashge3el3dif  14209  fi1uzind  14220  brfi1indALT  14223  swrdcl  14367  pfxcl  14399  relexpindlem  14783  fclim  15271  climmo  15275  rlimdmo1  15336  cicsym  17525  cictr  17526  brssc  17535  sscpwex  17536  initoid  17725  termoid  17726  initoeu1  17735  initoeu2lem1  17738  initoeu2  17740  termoeu1  17742  opifismgm  18352  grpidval  18354  dfgrp3e  18684  subgint  18788  giclcl  18897  gicrcl  18898  gicsym  18899  gicen  18902  gicsubgen  18903  cntzssv  18943  symgvalstruct  19013  symgvalstructOLD  19014  giccyg  19510  brric2  19998  ricgic  19999  subrgint  20055  lmiclcl  20341  lmicrcl  20342  lmicsym  20343  abvn0b  20582  lmiclbs  21053  lmisfree  21058  lmictra  21061  mpfrcl  21304  ply1frcl  21493  pf1rcl  21524  mat1scmat  21697  toprntopon  22083  topnex  22155  neitr  22340  cmpsub  22560  bwth  22570  iunconn  22588  2ndcsb  22609  unisngl  22687  elpt  22732  ptclsg  22775  hmphsym  22942  hmphen  22945  haushmphlem  22947  cmphmph  22948  connhmph  22949  reghmph  22953  nrmhmph  22954  hmphdis  22956  indishmph  22958  hmphen2  22959  ufldom  23122  alexsubALTlem2  23208  alexsubALT  23211  metustfbas  23722  iunmbl2  24730  ioorcl2  24745  ioorinv2  24748  opnmblALT  24776  plyssc  25370  aannenlem2  25498  mulog2sum  26694  istrkg2ld  26830  axcontlem4  27344  lfuhgr1v0e  27630  nbgr1vtx  27734  edgusgrnbfin  27749  cplgr1vlem  27805  cplgr1v  27806  fusgrn0degnn0  27875  g0wlk0  28028  wspthneq1eq2  28234  wlkswwlksf1o  28253  wwlksnndef  28279  wspthsnonn0vne  28291  eulerpath  28614  frgrwopreglem2  28686  friendship  28772  shintcli  29700  strlem1  30621  rexunirn  30849  iunrnmptss  30914  cnvoprabOLD  31064  lsmsnorb  31588  mxidlnzrb  31653  prsdm  31873  prsrn  31874  0elsiga  32091  sigaclcu  32094  issgon  32100  insiga  32114  omssubaddlem  32275  omssubadd  32276  bnj521  32725  bnj906  32919  bnj938  32926  bnj1018g  32952  bnj1018  32953  bnj1020  32954  bnj1125  32981  bnj1145  32982  funen1cnv  33069  fineqvac  33075  lfuhgr3  33090  loop1cycl  33108  satfrnmapom  33341  satf0op  33348  sat1el2xp  33350  dmopab3rexdif  33376  mppspstlem  33542  sslttr  34010  txpss3v  34189  pprodss4v  34195  elsingles  34229  fnimage  34240  funpartlem  34253  funpartfun  34254  dfrdg4  34262  colinearex  34371  bj-cleljusti  34870  axc11n11r  34874  bj-exlimvmpi  35105  bj-snglex  35172  bj-bm1.3ii  35244  bj-restpw  35272  mptsnunlem  35518  ctbssinf  35586  pibt2  35597  wl-moteq  35682  wl-sbcom2d  35725  wl-mo3t  35740  ptrecube  35786  mblfinlem3  35825  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  indexdom  35901  xrnss3v  36509  prtlem16  36890  sn-iotauni  40200  sn-iotanul  40201  sn-iotaex  40204  sbccomieg  40622  setindtr  40853  setindtrs  40854  dfac11  40894  lnmlmic  40920  gicabl  40931  isnumbasgrplem1  40933  iscard4  41147  rtrclex  41232  clcnvlem  41238  brtrclfv2  41342  snhesn  41401  frege55b  41512  frege55c  41533  grucollcld  41885  grumnudlem  41910  iotain  42042  iotavalb  42055  sbiota1  42059  iunconnlem2  42562  fnchoice  42579  stoweidlem59  43607  vitali2  44239  nsssmfmbf  44324  fsetprcnexALT  44567  funop1  44786  sbcpr  44984  opmpoismgm  45372  nzerooringczr  45641  mo0sn  46172  mofmo  46185  mofeu  46186  f1mo  46191  neircl  46209  fullthinc  46338  setrec1lem3  46406  elsetrecs  46416  elpglem1  46427