Theorem exlimiv 1965

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

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

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  exlimiiv  1966  exlimivv  1967  exsbim  2037  ax8  2153  ax9  2161  dfeumo  2564  mo3  2592  mo4  2594  moanimv  2647  euanv  2652  mopick  2653  clelab  2908  rexlimiva  3159  gencl  3495  cgsexg  3498  gencbvex2  3511  vtocleg  3520  eqvincg  3605  elrabi  3644  sbcex2  3802  sbccomlem  3821  eluni  4875  intab  4943  uniintsn  4950  dfiun2g  4993  disjiun  5096  trintss  5237  axrep6g  5249  sepexlem  5260  intex  5312  axpweq  5319  eunex  5359  eusvnf  5361  eusvnfb  5362  reusv2lem3  5369  axprglem  5401  axprg  5402  unipw  5425  moabex  5433  moabexOLD  5434  nnullss  5437  exss  5438  sbcop1  5465  cotsexgw  5470  mosubopt  5489  mosubott  5491  opelopabsb  5511  elrelb  5784  relop  5838  dmopab2rex  5911  dmrnssfld  5968  dmsnopg  6233  coass  6290  unixp0  6310  elsnxp  6320  iotauni2  6536  iotanul2  6537  iotain  6539  iotaex  6541  iotauni  6542  iota1  6544  iota4  6546  dffv2  7011  fveqdmss  7110  eldmrexrnb  7124  exfo  7137  funop  7185  funopdmsn  7186  funsndifnop  7187  csbriota  7423  eusvobj2  7443  fnoprabg  7574  limuni3  7897  tfindsg  7906  findsg  7943  elxp5  7969  f1oexbi  7974  ffoss  7992  fo1stres  8061  fo2ndres  8062  eloprabi  8109  frxp  8175  suppimacnv  8229  mpoxneldm  8267  mpoxopxnop0  8270  reldmtpos  8289  dftpos4  8300  frrlem2  8343  frrlem3  8344  frrlem4  8345  frrlem8  8349  tfrlem9  8431  ecdmn0  8808  mapprc  8889  fsetprcnex  8922  ixpprc  8985  ixpn0  8996  bren  9021  brdomg  9023  domssl  9063  domssr  9064  ener  9066  en0  9083  en0ALT  9084  en0r  9085  en1  9089  en1b  9090  funen1cnv  9094  2dom  9096  fiprc  9110  dom0  9162  pwdom  9186  domssex  9195  ssenen  9208  dif1en  9215  findcard2s  9219  ensymfib  9237  php  9260  sdom1  9279  1sdom2dom  9283  isinf  9294  en1eqsn  9304  infn0  9332  pwfir  9346  fodomfir  9357  hartogslem1  9573  brwdom  9598  brwdomn0  9600  wdompwdom  9609  unxpwdom2  9619  ixpiunwdom  9621  elirrvOLD  9629  infeq5  9675  brttrcl  9751  ttrcltr  9754  dmttrcl  9759  rnttrcl  9760  epfrs  9769  rankwflemb  9837  rankwflembOLD  9838  scottex  9970  bnd2  9993  setrec1lem3  10006  oncard  10078  carduni  10101  pm54.43  10121  ween  10153  acnrcl  10160  acndom  10169  acndom2  10172  iunfictbso  10232  aceq3lem  10238  dfac4  10240  dfac5lem4  10244  dfac5lem5  10245  dfac5  10246  dfac2a  10247  dfac2b  10248  dfacacn  10259  dfac12r  10264  kmlem2  10269  kmlem16  10283  ackbij2  10359  cff  10364  cardcf  10368  cfeq0  10373  cfsuc  10374  cff1  10375  cfcoflem  10389  coftr  10390  infpssr  10425  fin4en1  10426  isfin4-2  10431  enfin2i  10438  fin23lem21  10456  fin23lem30  10459  fin23lem41  10469  enfin1ai  10501  fin1a2lem7  10523  domtriomlem  10559  axdc2lem  10565  axdc3lem2  10568  axdc4lem  10572  axcclem  10574  ac6s  10601  zorn2lem7  10619  ttukey2g  10633  axdc  10638  brdom3  10646  brdom5  10647  brdom4  10648  brdom7disj  10649  brdom6disj  10650  konigthlem  10692  pwfseq  10788  tsk0  10887  gruina  10942  ltbtwnnq  11102  reclem2pr  11172  supsrlem  11235  supsr  11236  axpre-sup  11293  dedekindle  11513  nnunb  12642  ioorebas  13622  fzn0  13711  fzon0  13852  axdc4uzlem  14166  hasheqf1oi  14536  hash1snb  14605  hash1n0  14607  hashf1lem2  14642  hashle2pr  14663  hashge2el2difr  14667  hashge3el3dif  14673  fi1uzind  14693  brfi1indALT  14696  swrdcl  14835  pfxcl  14869  relexpindlem  15259  fclim  15764  climmo  15768  rlimdmo1  15829  cicsym  18029  cictr  18030  brssc  18039  sscpwex  18040  initoid  18226  termoid  18227  initoeu1  18236  initoeu2lem1  18239  initoeu2  18241  termoeu1  18243  opifismgm  18887  grpidval  18890  dfgrp3e  19300  subgint  19411  giclcl  19538  gicrcl  19539  gicsym  19540  gicen  19543  gicsubgen  19544  cntzssv  19593  symgvalstruct  19662  giccyg  20165  riclcl  20800  ricrcl  20801  ricsym  20802  isbrric2  20804  ricgic  20806  subrngint  20863  subrgint  20898  abvn0b  21144  lmiclcl  21396  lmicrcl  21397  lmicsym  21398  nzerooringczr  21841  lmiclbs  22198  lmisfree  22203  lmictra  22206  mpfrcl  22449  ply1frcl  22691  pf1rcl  22722  mat1scmat  22909  toprntopon  23298  topnex  23369  neitr  23553  cmpsub  23773  bwth  23783  iunconn  23801  2ndcsb  23822  unisngl  23901  elpt  23946  ptclsg  23989  hmphsym  24156  hmphen  24159  haushmphlem  24161  cmphmph  24162  connhmph  24163  reghmph  24167  nrmhmph  24168  hmphdis  24170  indishmph  24172  hmphen2  24173  ufldom  24336  alexsubALTlem2  24422  alexsubALT  24425  metustfbas  24931  iunmbl2  25933  ioorcl2  25948  ioorinv2  25951  opnmblALT  25979  plyssc  26573  aannenlem2  26713  sltstr  28230  oncutlt  28707  istrkg2ld  28979  axcontlem4  29602  lfuhgr3  29785  lfuhgr1v0e  29892  nbgr1vtx  29996  edgusgrnbfin  30011  cplgr1vlem  30067  cplgr1v  30068  fusgrn0degnn0  30137  g0wlk0  30288  wspthneq1eq2  30506  wlkswwlksf1o  30525  wwlksnndef  30551  wspthsnonn0vne  30563  loop1cycl  30801  eulerpath  30899  frgrwopreglem2  30971  friendship  31057  shintcli  31988  strlem1  32909  rexunirn  33187  iunrnmptss  33257  lsmsnorb  34050  mxidlnzrb  34108  prsdm  34657  prsrn  34658  0elsiga  34857  sigaclcu  34860  issgon  34866  insiga  34881  omssubaddlem  35042  omssubadd  35043  bnj906  35671  bnj938  35678  bnj1018g  35704  bnj1018  35705  bnj1020  35706  bnj1125  35733  bnj1145  35734  abweex  35842  axprALT2  35857  rankscott  35879  rankscottu  35880  dfac15  35886  acwer1prc  35893  fineqvac  35925  fineqvnttrclselem1  35930  fineqvnttrclselem2  35931  onvf1odlem4  36075  vonf1oonfo  36090  satfrnmapom  36343  satf0op  36350  sat1el2xp  36352  dmopab3rexdif  36378  mppspstlem  36544  elpssex  36672  elpssmo  36673  txpss3v  36855  pprodss4v  36861  elsingles  36895  fnimage  36906  funpartlem  36921  funpartfun  36922  dfrdg4  36930  colinearex  37040  dfttc4  37533  ttcexg  37535  regsfromregtco  37541  bj-cleljusti  37794  axc11n11r  37800  bj-exlimvmpi  38038  bj-snglex  38101  bj-unexg  38166  bj-bm1.3ii  38249  bj-axseprep  38260  bj-restpw  38283  mptsnunlem  38529  ctbssinf  38597  pibt2  38608  wl-ax12v2cl  38697  wl-moteq  38714  wl-sbcom2d  38761  wl-mo3t  38776  ptrecube  38806  mblfinlem3  38845  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  dfprop1  38913  indexdom  38936  xrnss3v  39579  prtlem16  40192  riccrng1  43848  ricdrng1  43858  sbccomieg  44066  setindtr  44297  setindtrs  44298  dfac11  44330  lnmlmic  44356  gicabl  44367  isnumbasgrplem1  44368  iscard4  44795  rtrclex  44878  clcnvlem  44884  brtrclfv2  44988  snhesn  45047  frege55b  45158  frege55c  45179  grucollcld  45505  grumnudlem  45530  iotavalb  45674  sbiota1  45678  iunconnlem2  46177  permaxun  46265  permac8prim  46268  hfstructfun  46293  rnhfstructhf  46296  hfstructhf  46297  hfstructcan  46298  fnchoice  46320  stoweidlem59  47342  vitali2  47977  nsssmfmbf  48062  fsetprcnexALT  48405  funop1  48626  sbcpr  48876  gricen  49296  grlicsym  49384  grlictr  49386  grlicen  49388  gricgrlic  49389  usgrexmpl12ngric  49409  usgrexmpl12ngrlic  49410  opmpoismgm  49537  mo0sn  50258  mofmo  50289  mofeu  50290  f1mo  50295  eloprab1st2nd  50310  neircl  50350  sectrcl  50467  invrcl  50469  isorcl  50478  isoval2  50480  initc  50537  uobffth  50665  uobeqw  50666  fullthinc  50916  termco  50947  termcbasmo  50949  isinito3  50966  oppctermhom  50970  functermc  50974  termc2  50984  eufunclem  50987  eufunc  50988  euendfunc  50992  arweuthinc  50995  arweutermc  50996  discsntermlem  51039  rellan  51137  relran  51138  termolmd  51184  elsetrecs  51199  elpglem1  51210