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  20913  lmicrcl  20914  lmicsym  20915  abvn0b  21208  nzerooringczr  21339  lmiclbs  21701  lmisfree  21706  lmictra  21709  mpfrcl  21958  ply1frcl  22156  pf1rcl  22187  mat1scmat  22360  toprntopon  22746  topnex  22818  neitr  23003  cmpsub  23223  bwth  23233  iunconn  23251  2ndcsb  23272  unisngl  23350  elpt  23395  ptclsg  23438  hmphsym  23605  hmphen  23608  haushmphlem  23610  cmphmph  23611  connhmph  23612  reghmph  23616  nrmhmph  23617  hmphdis  23619  indishmph  23621  hmphen2  23622  ufldom  23785  alexsubALTlem2  23871  alexsubALT  23874  metustfbas  24385  iunmbl2  25405  ioorcl2  25420  ioorinv2  25423  opnmblALT  25451  plyssc  26051  aannenlem2  26180  mulog2sum  27382  sslttr  27652  istrkg2ld  28143  axcontlem4  28657  lfuhgr1v0e  28943  nbgr1vtx  29047  edgusgrnbfin  29062  cplgr1vlem  29118  cplgr1v  29119  fusgrn0degnn0  29188  g0wlk0  29341  wspthneq1eq2  29546  wlkswwlksf1o  29565  wwlksnndef  29591  wspthsnonn0vne  29603  eulerpath  29926  frgrwopreglem2  29998  friendship  30084  shintcli  31014  strlem1  31935  rexunirn  32164  iunrnmptss  32229  cnvoprabOLD  32377  lsmsnorb  32940  mxidlnzrb  33034  prsdm  33357  prsrn  33358  0elsiga  33575  sigaclcu  33578  issgon  33584  insiga  33598  omssubaddlem  33761  omssubadd  33762  bnj906  34404  bnj938  34411  bnj1018g  34437  bnj1018  34438  bnj1020  34439  bnj1125  34466  bnj1145  34467  funen1cnv  34554  fineqvac  34560  lfuhgr3  34573  loop1cycl  34591  satfrnmapom  34824  satf0op  34831  sat1el2xp  34833  dmopab3rexdif  34859  mppspstlem  35025  txpss3v  35319  pprodss4v  35325  elsingles  35359  fnimage  35370  funpartlem  35383  funpartfun  35384  dfrdg4  35392  colinearex  35501  bj-cleljusti  36020  axc11n11r  36024  bj-exlimvmpi  36254  bj-snglex  36317  bj-unexg  36382  bj-bm1.3ii  36408  bj-restpw  36436  mptsnunlem  36682  ctbssinf  36750  pibt2  36761  wl-moteq  36846  wl-sbcom2d  36889  wl-mo3t  36904  ptrecube  36951  mblfinlem3  36990  ovoliunnfl  36993  voliunnfl  36995  volsupnfl  36996  indexdom  37065  xrnss3v  37705  prtlem16  38202  ricsym  41558  riccrng1  41560  ricdrng1  41566  sbccomieg  41993  setindtr  42225  setindtrs  42226  dfac11  42266  lnmlmic  42292  gicabl  42303  isnumbasgrplem1  42305  iscard4  42746  rtrclex  42830  clcnvlem  42836  brtrclfv2  42940  snhesn  42999  frege55b  43110  frege55c  43131  grucollcld  43481  grumnudlem  43506  iotain  43638  iotavalb  43651  sbiota1  43655  iunconnlem2  44158  fnchoice  44175  stoweidlem59  45233  vitali2  45868  nsssmfmbf  45953  fsetprcnexALT  46230  funop1  46449  sbcpr  46647  opmpoismgm  47003  mo0sn  47661  mofmo  47674  mofeu  47675  f1mo  47680  neircl  47698  fullthinc  47827  setrec1lem3  47895  elsetrecs  47906  elpglem1  47917