Theorem exlimiv 1928

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

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

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

Syntax hints:   → wi 4  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207  df-ex 1777

This theorem is referenced by:  exlimiiv  1929  exlimivv  1930  exsbim  1999  ax8  2112  ax9  2120  dfeumo  2535  mo3  2562  mo4  2564  moanimv  2617  euanv  2622  mopick  2623  clelab  2885  rexlimiva  3145  gencl  3521  cgsexg  3524  ceqsexvOLD  3531  gencbvex2  3542  vtocleg  3553  vtoclgOLD  3571  eqvincg  3648  elrabi  3690  sbcex2  3856  sbccomlem  3878  eluni  4915  intab  4983  uniintsn  4990  dfiun2g  5035  disjiun  5136  trintss  5284  axrep6g  5296  sepexlem  5305  intex  5350  axpweq  5357  eunex  5396  eusvnf  5398  eusvnfb  5399  reusv2lem3  5406  unipw  5461  moabex  5470  nnullss  5473  exss  5474  sbcop1  5499  mosubopt  5520  opelopabsb  5540  relop  5864  dmopab2rex  5931  dmrnssfld  5987  dmsnopg  6235  unixp0  6305  elsnxp  6313  iotauni2  6532  iotanul2  6533  iotaex  6536  iotauni  6538  iota1  6540  iota4  6544  dffv2  7004  fveqdmss  7098  eldmrexrnb  7112  exfo  7125  funop  7169  funopdmsn  7170  funsndifnop  7171  csbriota  7403  eusvobj2  7423  fnoprabg  7556  limuni3  7873  tfindsg  7882  findsg  7920  elxp5  7946  f1oexbi  7951  ffoss  7969  fo1stres  8039  fo2ndres  8040  eloprabi  8087  frxp  8150  suppimacnv  8198  mpoxneldm  8236  mpoxopxnop0  8239  reldmtpos  8258  dftpos4  8269  frrlem2  8311  frrlem3  8312  frrlem4  8313  frrlem8  8317  wfrlem2OLD  8348  wfrlem3OLD  8349  wfrlem4OLD  8351  wfrdmclOLD  8356  wfrlem12OLD  8359  tfrlem9  8424  ecdmn0  8793  mapprc  8869  fsetprcnex  8901  ixpprc  8958  ixpn0  8969  bren  8994  brdomg  8996  brdomgOLD  8997  domssl  9037  domssr  9038  ener  9040  en0  9057  en0ALT  9058  en0r  9059  en1  9063  en1b  9064  2dom  9069  fiprc  9084  dom0  9141  pwdom  9168  domssex  9177  ssenen  9190  rexdif1enOLD  9198  dif1en  9199  dif1enOLD  9201  findcard2s  9204  ensymfib  9222  php  9245  phpOLD  9257  sdom1  9276  1sdom2dom  9281  isinf  9294  isinfOLD  9295  en1eqsn  9306  infn0  9338  pwfir  9353  fodomfir  9366  hartogslem1  9580  brwdom  9605  brwdomn0  9607  wdompwdom  9616  unxpwdom2  9626  ixpiunwdom  9628  infeq5  9675  omex  9681  brttrcl  9751  ttrcltr  9754  dmttrcl  9759  rnttrcl  9760  epfrs  9769  rankwflemb  9831  bnd2  9931  oncard  9998  carduni  10019  pm54.43  10039  ween  10073  acnrcl  10080  acndom  10089  acndom2  10092  iunfictbso  10152  aceq3lem  10158  dfac4  10160  dfac5lem4  10164  dfac5lem5  10165  dfac5lem4OLD  10166  dfac5  10167  dfac2a  10168  dfac2b  10169  dfacacn  10180  dfac12r  10185  kmlem2  10190  kmlem16  10204  ackbij2  10280  cff  10286  cardcf  10290  cfeq0  10294  cfsuc  10295  cff1  10296  cfcoflem  10310  coftr  10311  infpssr  10346  fin4en1  10347  isfin4-2  10352  enfin2i  10359  fin23lem21  10377  fin23lem30  10380  fin23lem41  10390  enfin1ai  10422  fin1a2lem7  10444  domtriomlem  10480  axdc2lem  10486  axdc3lem2  10489  axdc4lem  10493  axcclem  10495  ac6s  10522  zorn2lem7  10540  ttukey2g  10554  axdc  10559  brdom3  10566  brdom5  10567  brdom4  10568  brdom7disj  10569  brdom6disj  10570  konigthlem  10606  pwcfsdom  10621  pwfseq  10702  tsk0  10801  gruina  10856  ltbtwnnq  11016  reclem2pr  11086  supsrlem  11149  supsr  11150  axpre-sup  11207  dedekindle  11423  nnunb  12520  ioorebas  13488  fzn0  13575  fzon0  13714  axdc4uzlem  14021  hasheqf1oi  14387  hash1snb  14455  hash1n0  14457  hashf1lem2  14492  hashle2pr  14513  hashge2el2difr  14517  hashge3el3dif  14523  fi1uzind  14543  brfi1indALT  14546  swrdcl  14680  pfxcl  14712  relexpindlem  15099  fclim  15586  climmo  15590  rlimdmo1  15651  cicsym  17852  cictr  17853  brssc  17862  sscpwex  17863  initoid  18055  termoid  18056  initoeu1  18065  initoeu2lem1  18068  initoeu2  18070  termoeu1  18072  opifismgm  18685  grpidval  18687  dfgrp3e  19071  subgint  19181  giclcl  19304  gicrcl  19305  gicsym  19306  gicen  19309  gicsubgen  19310  cntzssv  19359  symgvalstruct  19429  symgvalstructOLD  19430  giccyg  19933  brric2  20523  ricgic  20524  subrngint  20577  subrgint  20612  abvn0b  20854  lmiclcl  21087  lmicrcl  21088  lmicsym  21089  nzerooringczr  21509  lmiclbs  21875  lmisfree  21880  lmictra  21883  mpfrcl  22127  ply1frcl  22338  pf1rcl  22369  mat1scmat  22561  toprntopon  22947  topnex  23019  neitr  23204  cmpsub  23424  bwth  23434  iunconn  23452  2ndcsb  23473  unisngl  23551  elpt  23596  ptclsg  23639  hmphsym  23806  hmphen  23809  haushmphlem  23811  cmphmph  23812  connhmph  23813  reghmph  23817  nrmhmph  23818  hmphdis  23820  indishmph  23822  hmphen2  23823  ufldom  23986  alexsubALTlem2  24072  alexsubALT  24075  metustfbas  24586  iunmbl2  25606  ioorcl2  25621  ioorinv2  25624  opnmblALT  25652  plyssc  26254  aannenlem2  26386  mulog2sum  27596  sslttr  27867  istrkg2ld  28483  axcontlem4  28997  lfuhgr1v0e  29286  nbgr1vtx  29390  edgusgrnbfin  29405  cplgr1vlem  29461  cplgr1v  29462  fusgrn0degnn0  29532  g0wlk0  29685  wspthneq1eq2  29890  wlkswwlksf1o  29909  wwlksnndef  29935  wspthsnonn0vne  29947  eulerpath  30270  frgrwopreglem2  30342  friendship  30428  shintcli  31358  strlem1  32279  rexunirn  32520  iunrnmptss  32586  cnvoprabOLD  32738  lsmsnorb  33399  mxidlnzrb  33488  prsdm  33875  prsrn  33876  0elsiga  34095  sigaclcu  34098  issgon  34104  insiga  34118  omssubaddlem  34281  omssubadd  34282  bnj906  34923  bnj938  34930  bnj1018g  34956  bnj1018  34957  bnj1020  34958  bnj1125  34985  bnj1145  34986  funen1cnv  35081  fineqvac  35090  lfuhgr3  35104  loop1cycl  35122  satfrnmapom  35355  satf0op  35362  sat1el2xp  35364  dmopab3rexdif  35390  mppspstlem  35556  txpss3v  35860  pprodss4v  35866  elsingles  35900  fnimage  35911  funpartlem  35924  funpartfun  35925  dfrdg4  35933  colinearex  36042  bj-cleljusti  36662  axc11n11r  36666  bj-exlimvmpi  36894  bj-snglex  36956  bj-unexg  37021  bj-bm1.3ii  37047  bj-restpw  37075  mptsnunlem  37321  ctbssinf  37389  pibt2  37400  wl-ax12v2cl  37487  wl-moteq  37495  wl-sbcom2d  37542  wl-mo3t  37557  ptrecube  37607  mblfinlem3  37646  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  indexdom  37721  xrnss3v  38354  prtlem16  38851  ricsym  42506  riccrng1  42508  ricdrng1  42515  sbccomieg  42781  setindtr  43013  setindtrs  43014  dfac11  43051  lnmlmic  43077  gicabl  43088  isnumbasgrplem1  43090  iscard4  43523  rtrclex  43607  clcnvlem  43613  brtrclfv2  43717  snhesn  43776  frege55b  43887  frege55c  43908  grucollcld  44256  grumnudlem  44281  iotain  44413  iotavalb  44426  sbiota1  44430  iunconnlem2  44933  fnchoice  44967  stoweidlem59  46015  vitali2  46650  nsssmfmbf  46735  fsetprcnexALT  47012  funop1  47233  sbcpr  47446  gricen  47832  grlicsym  47909  grlictr  47911  grlicen  47913  gricgrlic  47914  usgrexmpl12ngric  47933  usgrexmpl12ngrlic  47934  opmpoismgm  48011  mo0sn  48664  mofmo  48677  mofeu  48678  f1mo  48683  neircl  48701  fullthinc  48846  setrec1lem3  48920  elsetrecs  48931  elpglem1  48942