Theorem exlimiv 1962

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

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

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  exlimiiv  1963  exlimivv  1964  exsbim  2034  ax8  2150  ax9  2158  dfeumo  2561  mo3  2589  mo4  2591  moanimv  2644  euanv  2649  mopick  2650  clelab  2904  rexlimiva  3155  gencl  3491  cgsexg  3494  gencbvex2  3507  vtocleg  3516  eqvincg  3601  elrabi  3640  sbcex2  3798  sbccomlem  3816  eluni  4869  intab  4937  uniintsn  4944  dfiun2g  4987  disjiun  5090  trintss  5230  axrep6g  5242  sepexlem  5253  intex  5304  axpweq  5311  eunex  5351  eusvnf  5353  eusvnfb  5354  reusv2lem3  5361  axprglem  5393  axprg  5394  unipw  5417  moabex  5425  moabexOLD  5426  nnullss  5429  exss  5430  sbcop1  5457  cotsexgw  5462  mosubopt  5481  mosubott  5483  opelopabsb  5503  elrelb  5774  relop  5827  dmopab2rex  5898  dmrnssfld  5955  dmsnopg  6214  unixp0  6286  elsnxp  6294  iotauni2  6510  iotanul2  6511  iotaex  6514  iotauni  6515  iota1  6517  iota4  6519  dffv2  6981  fveqdmss  7079  eldmrexrnb  7093  exfo  7106  funop  7154  funopdmsn  7155  funsndifnop  7156  csbriota  7393  eusvobj2  7413  fnoprabg  7544  limuni3  7864  tfindsg  7873  findsg  7910  elxp5  7936  f1oexbi  7941  ffoss  7959  fo1stres  8028  fo2ndres  8029  eloprabi  8075  frxp  8141  suppimacnv  8195  mpoxneldm  8233  mpoxopxnop0  8236  reldmtpos  8255  dftpos4  8266  frrlem2  8309  frrlem3  8310  frrlem4  8311  frrlem8  8315  tfrlem9  8397  ecdmn0  8774  mapprc  8855  fsetprcnex  8888  ixpprc  8951  ixpn0  8962  bren  8987  brdomg  8989  domssl  9029  domssr  9030  ener  9032  en0  9049  en0ALT  9050  en0r  9051  en1  9055  en1b  9056  funen1cnv  9060  2dom  9062  fiprc  9076  dom0  9128  pwdom  9152  domssex  9161  ssenen  9174  dif1en  9181  findcard2s  9185  ensymfib  9203  php  9226  sdom1  9245  1sdom2dom  9249  isinf  9260  en1eqsn  9270  infn0  9298  pwfir  9312  fodomfir  9323  hartogslem1  9540  brwdom  9565  brwdomn0  9567  wdompwdom  9576  unxpwdom2  9586  ixpiunwdom  9588  elirrvOLD  9596  infeq5  9642  brttrcl  9718  ttrcltr  9721  dmttrcl  9726  rnttrcl  9727  epfrs  9736  rankwflemb  9804  rankwflembOLD  9805  scottex  9937  bnd2  9960  setrec1lem3  9973  oncard  10045  carduni  10066  pm54.43  10086  ween  10118  acnrcl  10125  acndom  10134  acndom2  10137  iunfictbso  10197  aceq3lem  10203  dfac4  10205  dfac5lem4  10209  dfac5lem5  10210  dfac5  10211  dfac2a  10212  dfac2b  10213  dfacacn  10224  dfac12r  10229  kmlem2  10234  kmlem16  10248  ackbij2  10324  cff  10329  cardcf  10333  cfeq0  10338  cfsuc  10339  cff1  10340  cfcoflem  10354  coftr  10355  infpssr  10390  fin4en1  10391  isfin4-2  10396  enfin2i  10403  fin23lem21  10421  fin23lem30  10424  fin23lem41  10434  enfin1ai  10466  fin1a2lem7  10488  domtriomlem  10524  axdc2lem  10530  axdc3lem2  10533  axdc4lem  10537  axcclem  10539  ac6s  10566  zorn2lem7  10584  ttukey2g  10598  axdc  10603  brdom3  10611  brdom5  10612  brdom4  10613  brdom7disj  10614  brdom6disj  10615  konigthlem  10657  pwfseq  10753  tsk0  10852  gruina  10907  ltbtwnnq  11067  reclem2pr  11137  supsrlem  11200  supsr  11201  axpre-sup  11258  dedekindle  11478  nnunb  12606  ioorebas  13586  fzn0  13675  fzon0  13816  axdc4uzlem  14130  hasheqf1oi  14499  hash1snb  14568  hash1n0  14570  hashf1lem2  14605  hashle2pr  14626  hashge2el2difr  14630  hashge3el3dif  14636  fi1uzind  14656  brfi1indALT  14659  swrdcl  14798  pfxcl  14832  relexpindlem  15222  fclim  15726  climmo  15730  rlimdmo1  15791  cicsym  17985  cictr  17986  brssc  17995  sscpwex  17996  initoid  18182  termoid  18183  initoeu1  18192  initoeu2lem1  18195  initoeu2  18197  termoeu1  18199  opifismgm  18843  grpidval  18846  dfgrp3e  19256  subgint  19367  giclcl  19493  gicrcl  19494  gicsym  19495  gicen  19498  gicsubgen  19499  cntzssv  19548  symgvalstruct  19617  giccyg  20120  riclcl  20755  ricrcl  20756  ricsym  20757  isbrric2  20759  ricgic  20761  subrngint  20818  subrgint  20853  abvn0b  21099  lmiclcl  21351  lmicrcl  21352  lmicsym  21353  nzerooringczr  21792  lmiclbs  22149  lmisfree  22154  lmictra  22157  mpfrcl  22400  ply1frcl  22642  pf1rcl  22673  mat1scmat  22860  toprntopon  23249  topnex  23320  neitr  23504  cmpsub  23724  bwth  23734  iunconn  23752  2ndcsb  23773  unisngl  23852  elpt  23897  ptclsg  23940  hmphsym  24107  hmphen  24110  haushmphlem  24112  cmphmph  24113  connhmph  24114  reghmph  24118  nrmhmph  24119  hmphdis  24121  indishmph  24123  hmphen2  24124  ufldom  24287  alexsubALTlem2  24373  alexsubALT  24376  metustfbas  24882  iunmbl2  25884  ioorcl2  25899  ioorinv2  25902  opnmblALT  25930  plyssc  26524  aannenlem2  26662  sltstr  28179  oncutlt  28656  istrkg2ld  28928  axcontlem4  29551  lfuhgr3  29734  lfuhgr1v0e  29841  nbgr1vtx  29945  edgusgrnbfin  29960  cplgr1vlem  30016  cplgr1v  30017  fusgrn0degnn0  30086  g0wlk0  30237  wspthneq1eq2  30455  wlkswwlksf1o  30474  wwlksnndef  30500  wspthsnonn0vne  30512  loop1cycl  30750  eulerpath  30848  frgrwopreglem2  30920  friendship  31006  shintcli  31937  strlem1  32858  rexunirn  33136  iunrnmptss  33207  lsmsnorb  33993  mxidlnzrb  34051  prsdm  34593  prsrn  34594  0elsiga  34793  sigaclcu  34796  issgon  34802  insiga  34817  omssubaddlem  34978  omssubadd  34979  bnj906  35607  bnj938  35614  bnj1018g  35640  bnj1018  35641  bnj1020  35642  bnj1125  35669  bnj1145  35670  abweex  35770  axprALT2  35787  rankscott  35807  rankscottu  35808  dfac15  35810  acwer1prc  35817  fineqvac  35841  fineqvnttrclselem1  35846  fineqvnttrclselem2  35847  onvf1odlem4  35954  vonf1oonfo  35969  satfrnmapom  36222  satf0op  36229  sat1el2xp  36231  dmopab3rexdif  36257  mppspstlem  36423  txpss3v  36733  pprodss4v  36739  elsingles  36773  fnimage  36784  funpartlem  36799  funpartfun  36800  dfrdg4  36808  colinearex  36918  dfttc4  37411  ttcexg  37413  regsfromregtco  37419  bj-cleljusti  37672  axc11n11r  37678  bj-exlimvmpi  37916  bj-snglex  37979  bj-unexg  38044  bj-bm1.3ii  38072  bj-axseprep  38083  bj-restpw  38106  mptsnunlem  38355  ctbssinf  38423  pibt2  38434  wl-ax12v2cl  38523  wl-moteq  38540  wl-sbcom2d  38587  wl-mo3t  38602  ptrecube  38632  mblfinlem3  38671  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  dfprop1  38739  indexdom  38762  xrnss3v  39407  prtlem16  40020  riccrng1  43676  ricdrng1  43686  sbccomieg  43894  setindtr  44125  setindtrs  44126  dfac11  44158  lnmlmic  44184  gicabl  44195  isnumbasgrplem1  44197  iscard4  44628  rtrclex  44711  clcnvlem  44717  brtrclfv2  44821  snhesn  44880  frege55b  44991  frege55c  45012  grucollcld  45338  grumnudlem  45363  iotain  45495  iotavalb  45508  sbiota1  45512  iunconnlem2  46011  permaxun  46095  permac8prim  46098  hfstructfun  46120  rnhfstructhf  46123  hfstructhf  46124  hfstructcan  46125  fnchoice  46140  stoweidlem59  47163  vitali2  47798  nsssmfmbf  47883  fsetprcnexALT  48226  funop1  48447  sbcpr  48697  gricen  49117  grlicsym  49205  grlictr  49207  grlicen  49209  gricgrlic  49210  usgrexmpl12ngric  49230  usgrexmpl12ngrlic  49231  opmpoismgm  49358  mo0sn  50021  mofmo  50052  mofeu  50053  f1mo  50058  eloprab1st2nd  50073  neircl  50113  sectrcl  50230  invrcl  50232  isorcl  50241  isoval2  50243  initc  50300  uobffth  50428  uobeqw  50429  fullthinc  50679  termco  50710  termcbasmo  50712  isinito3  50729  oppctermhom  50733  functermc  50737  termc2  50747  eufunclem  50750  eufunc  50751  euendfunc  50755  arweuthinc  50758  arweutermc  50759  discsntermlem  50802  rellan  50900  relran  50901  termolmd  50947  elsetrecs  50962  elpglem1  50973