Theorem exlimiv 1963

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

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

This inference, along with its many variants such as rexlimdv 3162, 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 3162. 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 2147. (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  2151  ax9  2159  dfeumo  2562  mo3  2590  mo4  2592  moanimv  2645  euanv  2650  mopick  2651  clelab  2905  rexlimiva  3156  gencl  3492  cgsexg  3495  gencbvex2  3508  vtocleg  3517  eqvincg  3602  elrabi  3641  sbcex2  3799  sbccomlem  3817  eluni  4870  intab  4938  uniintsn  4945  dfiun2g  4988  disjiun  5091  trintss  5231  axrep6g  5243  sepexlem  5254  intex  5305  axpweq  5312  eunex  5352  eusvnf  5354  eusvnfb  5355  reusv2lem3  5362  axprglem  5394  axprg  5395  unipw  5418  moabex  5426  moabexOLD  5427  nnullss  5430  exss  5431  sbcop1  5458  cotsexgw  5463  mosubopt  5482  mosubott  5484  opelopabsb  5504  elrelb  5775  relop  5828  dmopab2rex  5899  dmrnssfld  5956  dmsnopg  6213  unixp0  6285  elsnxp  6293  iotauni2  6509  iotanul2  6510  iotaex  6513  iotauni  6514  iota1  6516  iota4  6518  dffv2  6978  fveqdmss  7076  eldmrexrnb  7090  exfo  7103  funop  7151  funopdmsn  7152  funsndifnop  7153  csbriota  7390  eusvobj2  7410  fnoprabg  7541  limuni3  7861  tfindsg  7870  findsg  7907  elxp5  7933  f1oexbi  7938  ffoss  7956  fo1stres  8025  fo2ndres  8026  eloprabi  8072  frxp  8136  suppimacnv  8184  mpoxneldm  8222  mpoxopxnop0  8225  reldmtpos  8244  dftpos4  8255  frrlem2  8298  frrlem3  8299  frrlem4  8300  frrlem8  8304  tfrlem9  8386  ecdmn0  8763  mapprc  8844  fsetprcnex  8877  ixpprc  8940  ixpn0  8951  bren  8976  brdomg  8978  domssl  9018  domssr  9019  ener  9021  en0  9038  en0ALT  9039  en0r  9040  en1  9044  en1b  9045  funen1cnv  9049  2dom  9051  fiprc  9065  dom0  9117  pwdom  9141  domssex  9150  ssenen  9163  dif1en  9170  findcard2s  9174  ensymfib  9192  php  9215  sdom1  9234  1sdom2dom  9238  isinf  9249  en1eqsn  9259  infn0  9287  pwfir  9301  fodomfir  9312  hartogslem1  9529  brwdom  9554  brwdomn0  9556  wdompwdom  9565  unxpwdom2  9575  ixpiunwdom  9577  elirrvOLD  9585  infeq5  9631  brttrcl  9707  ttrcltr  9710  dmttrcl  9715  rnttrcl  9716  epfrs  9725  rankwflemb  9793  rankwflembOLD  9794  scottex  9926  bnd2  9949  setrec1lem3  9962  oncard  10034  carduni  10055  pm54.43  10075  ween  10107  acnrcl  10114  acndom  10123  acndom2  10126  iunfictbso  10186  aceq3lem  10192  dfac4  10194  dfac5lem4  10198  dfac5lem5  10199  dfac5  10200  dfac2a  10201  dfac2b  10202  dfacacn  10213  dfac12r  10218  kmlem2  10223  kmlem16  10237  ackbij2  10313  cff  10318  cardcf  10322  cfeq0  10327  cfsuc  10328  cff1  10329  cfcoflem  10343  coftr  10344  infpssr  10379  fin4en1  10380  isfin4-2  10385  enfin2i  10392  fin23lem21  10410  fin23lem30  10413  fin23lem41  10423  enfin1ai  10455  fin1a2lem7  10477  domtriomlem  10513  axdc2lem  10519  axdc3lem2  10522  axdc4lem  10526  axcclem  10528  ac6s  10555  zorn2lem7  10573  ttukey2g  10587  axdc  10592  brdom3  10600  brdom5  10601  brdom4  10602  brdom7disj  10603  brdom6disj  10604  konigthlem  10646  pwfseq  10742  tsk0  10841  gruina  10896  ltbtwnnq  11056  reclem2pr  11126  supsrlem  11189  supsr  11190  axpre-sup  11247  dedekindle  11467  nnunb  12595  ioorebas  13575  fzn0  13664  fzon0  13805  axdc4uzlem  14119  hasheqf1oi  14488  hash1snb  14557  hash1n0  14559  hashf1lem2  14594  hashle2pr  14615  hashge2el2difr  14619  hashge3el3dif  14625  fi1uzind  14645  brfi1indALT  14648  swrdcl  14786  pfxcl  14820  relexpindlem  15209  fclim  15713  climmo  15717  rlimdmo1  15778  cicsym  17972  cictr  17973  brssc  17982  sscpwex  17983  initoid  18169  termoid  18170  initoeu1  18179  initoeu2lem1  18182  initoeu2  18184  termoeu1  18186  opifismgm  18830  grpidval  18833  dfgrp3e  19243  subgint  19354  giclcl  19480  gicrcl  19481  gicsym  19482  gicen  19485  gicsubgen  19486  cntzssv  19535  symgvalstruct  19604  giccyg  20107  riclcl  20742  ricrcl  20743  ricsym  20744  isbrric2  20746  ricgic  20748  subrngint  20805  subrgint  20840  abvn0b  21086  lmiclcl  21338  lmicrcl  21339  lmicsym  21340  nzerooringczr  21779  lmiclbs  22136  lmisfree  22141  lmictra  22144  mpfrcl  22387  ply1frcl  22629  pf1rcl  22660  mat1scmat  22847  toprntopon  23236  topnex  23307  neitr  23491  cmpsub  23711  bwth  23721  iunconn  23739  2ndcsb  23760  unisngl  23839  elpt  23884  ptclsg  23927  hmphsym  24094  hmphen  24097  haushmphlem  24099  cmphmph  24100  connhmph  24101  reghmph  24105  nrmhmph  24106  hmphdis  24108  indishmph  24110  hmphen2  24111  ufldom  24274  alexsubALTlem2  24360  alexsubALT  24363  metustfbas  24869  iunmbl2  25871  ioorcl2  25886  ioorinv2  25889  opnmblALT  25917  plyssc  26511  aannenlem2  26649  sltstr  28166  oncutlt  28643  istrkg2ld  28915  axcontlem4  29538  lfuhgr3  29721  lfuhgr1v0e  29828  nbgr1vtx  29932  edgusgrnbfin  29947  cplgr1vlem  30003  cplgr1v  30004  fusgrn0degnn0  30073  g0wlk0  30224  wspthneq1eq2  30442  wlkswwlksf1o  30461  wwlksnndef  30487  wspthsnonn0vne  30499  loop1cycl  30737  eulerpath  30835  frgrwopreglem2  30907  friendship  30993  shintcli  31924  strlem1  32845  rexunirn  33081  iunrnmptss  33152  lsmsnorb  33939  mxidlnzrb  33997  prsdm  34539  prsrn  34540  0elsiga  34739  sigaclcu  34742  issgon  34748  insiga  34763  omssubaddlem  34924  omssubadd  34925  bnj906  35553  bnj938  35560  bnj1018g  35586  bnj1018  35587  bnj1020  35588  bnj1125  35615  bnj1145  35616  axprALT2  35723  rankscott  35740  rankscottu  35741  fineqvac  35767  fineqvnttrclselem1  35772  fineqvnttrclselem2  35773  onvf1odlem4  35868  vonf1oonfo  35877  satfrnmapom  36114  satf0op  36121  sat1el2xp  36123  dmopab3rexdif  36149  mppspstlem  36315  txpss3v  36620  pprodss4v  36626  elsingles  36660  fnimage  36671  funpartlem  36686  funpartfun  36687  dfrdg4  36695  colinearex  36805  dfttc4  37298  ttcexg  37300  regsfromregtco  37306  bj-cleljusti  37559  axc11n11r  37565  bj-exlimvmpi  37803  bj-snglex  37866  bj-unexg  37931  bj-bm1.3ii  37959  bj-axseprep  37970  bj-restpw  37993  mptsnunlem  38241  ctbssinf  38309  pibt2  38320  wl-ax12v2cl  38409  wl-moteq  38426  wl-sbcom2d  38473  wl-mo3t  38488  ptrecube  38518  mblfinlem3  38557  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  dfprop1  38625  indexdom  38648  xrnss3v  39293  prtlem16  39906  riccrng1  43562  ricdrng1  43572  sbccomieg  43779  setindtr  44010  setindtrs  44011  dfac11  44048  lnmlmic  44074  gicabl  44085  isnumbasgrplem1  44087  iscard4  44518  rtrclex  44602  clcnvlem  44608  brtrclfv2  44712  snhesn  44771  frege55b  44882  frege55c  44903  grucollcld  45229  grumnudlem  45254  iotain  45386  iotavalb  45399  sbiota1  45403  iunconnlem2  45902  permaxun  45979  permac8prim  45982  fnchoice  46015  stoweidlem59  47038  vitali2  47673  nsssmfmbf  47758  fsetprcnexALT  48101  funop1  48322  sbcpr  48572  gricen  48992  grlicsym  49080  grlictr  49082  grlicen  49084  gricgrlic  49085  usgrexmpl12ngric  49105  usgrexmpl12ngrlic  49106  opmpoismgm  49233  mo0sn  49895  mofmo  49926  mofeu  49927  f1mo  49932  eloprab1st2nd  49947  neircl  49982  sectrcl  50099  invrcl  50101  isorcl  50110  isoval2  50112  initc  50168  uobffth  50295  uobeqw  50296  fullthinc  50527  termco  50558  termcbasmo  50560  isinito3  50577  oppctermhom  50581  functermc  50585  termc2  50595  eufunclem  50598  eufunc  50599  euendfunc  50603  arweuthinc  50606  arweutermc  50607  discsntermlem  50647  rellan  50700  relran  50701  termolmd  50747  elsetrecs  50762  elpglem1  50773