Theorem exlimiv 1932

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

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

This inference, along with its many variants such as rexlimdv 3152, 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 3152. 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 1970 and ax-8 2107. (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 1836	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
3		ax5e 1914	. 2 ⊢ (∃𝑥𝜓 → 𝜓)
4	2, 3	syl 17	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1780

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

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

This theorem is referenced by:  exlimiiv  1933  exlimivv  1934  exsbim  2004  ax8  2111  ax9  2119  dfeumo  2530  mo3  2557  mo4  2559  moanimv  2614  euanv  2619  mopick  2620  clelab  2878  rexlimiva  3146  gencl  3515  cgsexg  3518  ceqsexvOLD  3526  gencbvex2  3536  vtocleg  3541  vtoclgOLD  3559  eqvincg  3636  elrabi  3677  elrabiOLD  3678  sbcex2  3842  eluni  4911  intab  4982  uniintsn  4991  dfiun2g  5033  disjiun  5135  trintss  5284  axrep6g  5293  intex  5337  axpweq  5348  eunex  5388  eusvnf  5390  eusvnfb  5391  reusv2lem3  5398  unipw  5450  moabex  5459  nnullss  5462  exss  5463  sbcop1  5488  mosubopt  5510  opelopabsb  5530  relop  5850  dmopab2rex  5917  dmrnssfld  5969  dmsnopg  6212  unixp0  6282  elsnxp  6290  iotauni2  6512  iotanul2  6513  iotaex  6516  iotauni  6518  iota1  6520  iota4  6524  dffv2  6986  fveqdmss  7080  eldmrexrnb  7093  exfo  7106  funop  7149  funopdmsn  7150  funsndifnop  7151  csbriota  7384  eusvobj2  7404  fnoprabg  7534  limuni3  7845  tfindsg  7854  findsg  7894  elxp5  7918  f1oexbi  7923  ffoss  7936  fo1stres  8005  fo2ndres  8006  eloprabi  8053  frxp  8117  suppimacnv  8164  mpoxneldm  8203  mpoxopxnop0  8206  reldmtpos  8225  dftpos4  8236  frrlem2  8278  frrlem3  8279  frrlem4  8280  frrlem8  8284  wfrlem2OLD  8315  wfrlem3OLD  8316  wfrlem4OLD  8318  wfrdmclOLD  8323  wfrlem12OLD  8326  tfrlem9  8391  ecdmn0  8756  mapprc  8830  fsetprcnex  8862  ixpprc  8919  ixpn0  8930  bren  8955  brenOLD  8956  brdomg  8958  brdomgOLD  8959  domssl  9000  domssr  9001  ener  9003  en0  9019  en0OLD  9020  en0ALT  9021  en0r  9022  en1  9027  en1OLD  9028  en1b  9029  en1bOLD  9030  2dom  9036  fiprc  9051  dom0  9108  pwdom  9135  domssex  9144  ssenen  9157  rexdif1enOLD  9165  dif1en  9166  dif1enOLD  9168  findcard2s  9171  pwfir  9182  ensymfib  9193  php  9216  phpOLD  9228  sdom1  9248  1sdom2dom  9253  isinf  9266  isinfOLD  9267  en1eqsn  9280  infn0  9313  hartogslem1  9543  brwdom  9568  brwdomn0  9570  wdompwdom  9579  unxpwdom2  9589  ixpiunwdom  9591  infeq5  9638  omex  9644  brttrcl  9714  ttrcltr  9717  dmttrcl  9722  rnttrcl  9723  epfrs  9732  rankwflemb  9794  bnd2  9894  oncard  9961  carduni  9982  pm54.43  10002  ween  10036  acnrcl  10043  acndom  10052  acndom2  10055  iunfictbso  10115  aceq3lem  10121  dfac4  10123  dfac5lem4  10127  dfac5lem5  10128  dfac5  10129  dfac2a  10130  dfac2b  10131  dfacacn  10142  dfac12r  10147  kmlem2  10152  kmlem16  10166  ackbij2  10244  cff  10249  cardcf  10253  cfeq0  10257  cfsuc  10258  cff1  10259  cfcoflem  10273  coftr  10274  infpssr  10309  fin4en1  10310  isfin4-2  10315  enfin2i  10322  fin23lem21  10340  fin23lem30  10343  fin23lem41  10353  enfin1ai  10385  fin1a2lem7  10407  domtriomlem  10443  axdc2lem  10449  axdc3lem2  10452  axdc4lem  10456  axcclem  10458  ac6s  10485  zorn2lem7  10503  ttukey2g  10517  axdc  10522  brdom3  10529  brdom5  10530  brdom4  10531  brdom7disj  10532  brdom6disj  10533  konigthlem  10569  pwcfsdom  10584  pwfseq  10665  tsk0  10764  gruina  10819  ltbtwnnq  10979  reclem2pr  11049  supsrlem  11112  supsr  11113  axpre-sup  11170  dedekindle  11385  nnunb  12475  ioorebas  13435  fzn0  13522  fzon0  13657  axdc4uzlem  13955  hasheqf1oi  14318  hash1snb  14386  hash1n0  14388  hashf1lem2  14424  hashle2pr  14445  hashge2el2difr  14449  hashge3el3dif  14454  fi1uzind  14465  brfi1indALT  14468  swrdcl  14602  pfxcl  14634  relexpindlem  15017  fclim  15504  climmo  15508  rlimdmo1  15569  cicsym  17758  cictr  17759  brssc  17768  sscpwex  17769  initoid  17961  termoid  17962  initoeu1  17971  initoeu2lem1  17974  initoeu2  17976  termoeu1  17978  opifismgm  18590  grpidval  18592  dfgrp3e  18966  subgint  19073  giclcl  19194  gicrcl  19195  gicsym  19196  gicen  19199  gicsubgen  19200  cntzssv  19240  symgvalstruct  19312  symgvalstructOLD  19313  giccyg  19816  brric2  20404  ricgic  20405  subrngint  20456  subrgint  20493  lmiclcl  20914  lmicrcl  20915  lmicsym  20916  abvn0b  21209  nzerooringczr  21340  lmiclbs  21702  lmisfree  21707  lmictra  21710  mpfrcl  21959  ply1frcl  22157  pf1rcl  22188  mat1scmat  22361  toprntopon  22747  topnex  22819  neitr  23004  cmpsub  23224  bwth  23234  iunconn  23252  2ndcsb  23273  unisngl  23351  elpt  23396  ptclsg  23439  hmphsym  23606  hmphen  23609  haushmphlem  23611  cmphmph  23612  connhmph  23613  reghmph  23617  nrmhmph  23618  hmphdis  23620  indishmph  23622  hmphen2  23623  ufldom  23786  alexsubALTlem2  23872  alexsubALT  23875  metustfbas  24386  iunmbl2  25406  ioorcl2  25421  ioorinv2  25424  opnmblALT  25452  plyssc  26052  aannenlem2  26181  mulog2sum  27383  sslttr  27653  istrkg2ld  28144  axcontlem4  28658  lfuhgr1v0e  28944  nbgr1vtx  29048  edgusgrnbfin  29063  cplgr1vlem  29119  cplgr1v  29120  fusgrn0degnn0  29189  g0wlk0  29342  wspthneq1eq2  29547  wlkswwlksf1o  29566  wwlksnndef  29592  wspthsnonn0vne  29604  eulerpath  29927  frgrwopreglem2  29999  friendship  30085  shintcli  31015  strlem1  31936  rexunirn  32165  iunrnmptss  32230  cnvoprabOLD  32378  lsmsnorb  32941  mxidlnzrb  33035  prsdm  33358  prsrn  33359  0elsiga  33576  sigaclcu  33579  issgon  33585  insiga  33599  omssubaddlem  33762  omssubadd  33763  bnj906  34405  bnj938  34412  bnj1018g  34438  bnj1018  34439  bnj1020  34440  bnj1125  34467  bnj1145  34468  funen1cnv  34555  fineqvac  34561  lfuhgr3  34574  loop1cycl  34592  satfrnmapom  34825  satf0op  34832  sat1el2xp  34834  dmopab3rexdif  34860  mppspstlem  35026  txpss3v  35320  pprodss4v  35326  elsingles  35360  fnimage  35371  funpartlem  35384  funpartfun  35385  dfrdg4  35393  colinearex  35502  bj-cleljusti  36021  axc11n11r  36025  bj-exlimvmpi  36255  bj-snglex  36318  bj-unexg  36383  bj-bm1.3ii  36409  bj-restpw  36437  mptsnunlem  36683  ctbssinf  36751  pibt2  36762  wl-moteq  36847  wl-sbcom2d  36890  wl-mo3t  36905  ptrecube  36952  mblfinlem3  36991  ovoliunnfl  36994  voliunnfl  36996  volsupnfl  36997  indexdom  37066  xrnss3v  37706  prtlem16  38203  ricsym  41559  riccrng1  41561  ricdrng1  41567  sbccomieg  41994  setindtr  42226  setindtrs  42227  dfac11  42267  lnmlmic  42293  gicabl  42304  isnumbasgrplem1  42306  iscard4  42747  rtrclex  42831  clcnvlem  42837  brtrclfv2  42941  snhesn  43000  frege55b  43111  frege55c  43132  grucollcld  43482  grumnudlem  43507  iotain  43639  iotavalb  43652  sbiota1  43656  iunconnlem2  44159  fnchoice  44176  stoweidlem59  45234  vitali2  45869  nsssmfmbf  45954  fsetprcnexALT  46231  funop1  46450  sbcpr  46648  opmpoismgm  47004  mo0sn  47662  mofmo  47675  mofeu  47676  f1mo  47681  neircl  47699  fullthinc  47828  setrec1lem3  47896  elsetrecs  47907  elpglem1  47918