Theorem exlimiv 1963

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

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

This inference, along with its many variants such as rexlimdv 3166, 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 3166. 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 1963 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1964. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 2000 and ax-8 2148. (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 1945	. 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 1943

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

This theorem is used by:  exlimiiv  1964  exlimivv  1965  exsbim  2035  ax8  2152  ax9  2160  dfeumo  2566  mo3  2594  mo4  2596  moanimv  2649  euanv  2654  mopick  2655  clelab  2909  rexlimiva  3160  gencl  3498  cgsexg  3501  gencbvex2  3514  vtocleg  3523  eqvincg  3609  elrabi  3648  sbcex2  3806  sbccomlem  3824  eluni  4877  intab  4945  uniintsn  4952  dfiun2g  4996  disjiun  5099  trintss  5239  axrep6g  5253  sepexlem  5264  intex  5316  axpweq  5323  eunex  5363  eusvnf  5365  eusvnfb  5366  reusv2lem3  5373  axprglem  5409  axprg  5410  unipw  5433  moabex  5441  moabexOLD  5442  nnullss  5445  exss  5446  sbcop1  5472  mosubopt  5495  opelopabsb  5516  relop  5838  dmopab2rex  5909  dmrnssfld  5966  dmsnopg  6216  unixp0  6288  elsnxp  6296  iotauni2  6512  iotanul2  6513  iotaex  6516  iotauni  6517  iota1  6519  iota4  6521  dffv2  6980  fveqdmss  7077  eldmrexrnb  7091  exfo  7104  funop  7150  funopdmsn  7151  funsndifnop  7152  csbriota  7388  eusvobj2  7408  fnoprabg  7539  limuni3  7850  tfindsg  7859  findsg  7896  elxp5  7922  f1oexbi  7927  ffoss  7945  fo1stres  8014  fo2ndres  8015  eloprabi  8062  frxp  8124  suppimacnv  8172  mpoxneldm  8210  mpoxopxnop0  8213  reldmtpos  8232  dftpos4  8243  frrlem2  8286  frrlem3  8287  frrlem4  8288  frrlem8  8292  tfrlem9  8374  ecdmn0  8749  mapprc  8830  fsetprcnex  8861  ixpprc  8919  ixpn0  8930  bren  8955  brdomg  8957  domssl  8997  domssr  8998  ener  9000  en0  9017  en0ALT  9018  en0r  9019  en1  9023  en1b  9024  funen1cnv  9028  2dom  9030  fiprc  9044  dom0  9096  pwdom  9120  domssex  9129  ssenen  9142  dif1en  9149  findcard2s  9153  ensymfib  9171  php  9194  sdom1  9213  1sdom2dom  9217  isinf  9228  en1eqsn  9238  infn0  9265  pwfir  9279  fodomfir  9290  hartogslem1  9507  brwdom  9532  brwdomn0  9534  wdompwdom  9543  unxpwdom2  9553  ixpiunwdom  9555  elirrvOLD  9563  infeq5  9609  brttrcl  9685  ttrcltr  9688  dmttrcl  9693  rnttrcl  9694  epfrs  9703  rankwflemb  9768  scottex  9865  bnd2  9888  oncard  9958  carduni  9979  pm54.43  9999  ween  10031  acnrcl  10038  acndom  10047  acndom2  10050  iunfictbso  10110  aceq3lem  10116  dfac4  10118  dfac5lem4  10122  dfac5lem5  10123  dfac5  10124  dfac2a  10125  dfac2b  10126  dfacacn  10137  dfac12r  10142  kmlem2  10147  kmlem16  10161  ackbij2  10237  cff  10242  cardcf  10246  cfeq0  10251  cfsuc  10252  cff1  10253  cfcoflem  10267  coftr  10268  infpssr  10303  fin4en1  10304  isfin4-2  10309  enfin2i  10316  fin23lem21  10334  fin23lem30  10337  fin23lem41  10347  enfin1ai  10379  fin1a2lem7  10401  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  axdc4lem  10450  axcclem  10452  ac6s  10479  zorn2lem7  10497  ttukey2g  10511  axdc  10516  brdom3  10523  brdom5  10524  brdom4  10525  brdom7disj  10526  brdom6disj  10527  konigthlem  10564  pwfseq  10660  tsk0  10759  gruina  10814  ltbtwnnq  10974  reclem2pr  11044  supsrlem  11107  supsr  11108  axpre-sup  11165  dedekindle  11385  nnunb  12511  ioorebas  13490  fzn0  13578  fzon0  13719  axdc4uzlem  14033  hasheqf1oi  14401  hash1snb  14470  hash1n0  14472  hashf1lem2  14507  hashle2pr  14528  hashge2el2difr  14532  hashge3el3dif  14538  fi1uzind  14558  brfi1indALT  14561  swrdcl  14699  pfxcl  14733  relexpindlem  15120  fclim  15624  climmo  15628  rlimdmo1  15689  cicsym  17879  cictr  17880  brssc  17889  sscpwex  17890  initoid  18076  termoid  18077  initoeu1  18086  initoeu2lem1  18089  initoeu2  18091  termoeu1  18093  opifismgm  18735  grpidval  18737  dfgrp3e  19130  subgint  19241  giclcl  19367  gicrcl  19368  gicsym  19369  gicen  19372  gicsubgen  19373  cntzssv  19422  symgvalstruct  19491  giccyg  19994  riclcl  20627  ricrcl  20628  ricsym  20629  isbrric2  20631  ricgic  20633  subrngint  20689  subrgint  20724  abvn0b  20969  lmiclcl  21221  lmicrcl  21222  lmicsym  21223  nzerooringczr  21660  lmiclbs  22017  lmisfree  22022  lmictra  22025  mpfrcl  22266  ply1frcl  22508  pf1rcl  22539  mat1scmat  22726  toprntopon  23112  topnex  23183  neitr  23367  cmpsub  23587  bwth  23597  iunconn  23615  2ndcsb  23636  unisngl  23715  elpt  23760  ptclsg  23803  hmphsym  23970  hmphen  23973  haushmphlem  23975  cmphmph  23976  connhmph  23977  reghmph  23981  nrmhmph  23982  hmphdis  23984  indishmph  23986  hmphen2  23987  ufldom  24150  alexsubALTlem2  24236  alexsubALT  24239  metustfbas  24745  iunmbl2  25747  ioorcl2  25762  ioorinv2  25765  opnmblALT  25793  plyssc  26388  aannenlem2  26523  sltstr  28011  oncutlt  28488  istrkg2ld  28760  axcontlem4  29348  lfuhgr3  29531  lfuhgr1v0e  29638  nbgr1vtx  29742  edgusgrnbfin  29757  cplgr1vlem  29813  cplgr1v  29814  fusgrn0degnn0  29883  g0wlk0  30034  wspthneq1eq2  30252  wlkswwlksf1o  30271  wwlksnndef  30297  wspthsnonn0vne  30309  loop1cycl  30547  eulerpath  30639  frgrwopreglem2  30711  friendship  30797  shintcli  31728  strlem1  32649  rexunirn  32885  iunrnmptss  32957  lsmsnorb  33744  mxidlnzrb  33802  prsdm  34344  prsrn  34345  0elsiga  34544  sigaclcu  34547  issgon  34553  insiga  34568  omssubaddlem  34730  omssubadd  34731  bnj906  35359  bnj938  35366  bnj1018g  35392  bnj1018  35393  bnj1020  35394  bnj1125  35421  bnj1145  35422  axprALT2  35537  rankscott  35555  rankscottu  35556  fineqvac  35562  fineqvnttrclselem1  35567  fineqvnttrclselem2  35568  onvf1odlem4  35623  vonf1oonfo  35632  satfrnmapom  35875  satf0op  35882  sat1el2xp  35884  dmopab3rexdif  35910  mppspstlem  36076  txpss3v  36381  pprodss4v  36387  elsingles  36421  fnimage  36432  funpartlem  36447  funpartfun  36448  dfrdg4  36456  colinearex  36565  dfttc4  37074  ttcexg  37076  regsfromregtco  37082  bj-cleljusti  37335  axc11n11r  37341  bj-exlimvmpi  37579  bj-snglex  37642  bj-unexg  37707  bj-bm1.3ii  37733  bj-axseprep  37744  bj-restpw  37767  mptsnunlem  38017  ctbssinf  38085  pibt2  38096  wl-ax12v2cl  38185  wl-moteq  38202  wl-sbcom2d  38249  wl-mo3t  38264  ptrecube  38304  mblfinlem3  38343  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  indexdom  38418  xrnss3v  39063  prtlem16  39676  riccrng1  43322  ricdrng1  43329  sbccomieg  43553  setindtr  43784  setindtrs  43785  dfac11  43822  lnmlmic  43848  gicabl  43859  isnumbasgrplem1  43861  iscard4  44292  rtrclex  44376  clcnvlem  44382  brtrclfv2  44486  snhesn  44545  frege55b  44656  frege55c  44677  grucollcld  45003  grumnudlem  45028  iotain  45160  iotavalb  45173  sbiota1  45177  iunconnlem2  45676  permaxun  45753  permac8prim  45756  fnchoice  45782  stoweidlem59  46806  vitali2  47441  nsssmfmbf  47526  fsetprcnexALT  47832  funop1  48053  sbcpr  48303  gricen  48723  grlicsym  48811  grlictr  48813  grlicen  48815  gricgrlic  48816  usgrexmpl12ngric  48836  usgrexmpl12ngrlic  48837  opmpoismgm  48965  mo0sn  49627  mofmo  49658  mofeu  49659  f1mo  49664  eloprab1st2nd  49679  neircl  49716  sectrcl  49833  invrcl  49835  isorcl  49844  isoval2  49846  initc  49902  uobffth  50029  uobeqw  50030  fullthinc  50261  termco  50292  termcbasmo  50294  isinito3  50311  oppctermhom  50315  functermc  50319  termc2  50329  eufunclem  50332  eufunc  50333  euendfunc  50337  arweuthinc  50340  arweutermc  50341  discsntermlem  50381  rellan  50434  relran  50435  termolmd  50481  setrec1lem3  50500  elsetrecs  50511  elpglem1  50522