Theorem exlimiv 1845

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

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

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

Syntax hints:   → wi 4  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  exlimiiv  1846  exlimivv  1847  equvinv  1946  equvinvOLD  1949  ax8  1983  ax9  1990  19.8aOLD  2040  sbcom2  2433  euex  2482  mo3  2495  mopick  2523  gencl  3208  cgsexg  3211  gencbvex2  3224  vtocleg  3252  eqvinc  3300  elrabi  3328  sbcex2  3453  eluni  4375  intab  4442  uniintsn  4449  disjiun  4573  trint0  4698  intex  4747  axpweq  4768  eunex  4785  eusvnf  4787  eusvnfb  4788  reusv2lem3  4797  unipw  4845  moabex  4854  nnullss  4857  exss  4858  mosubopt  4897  opelopabsb  4910  relop  5194  dmrnssfld  5305  dmsnopg  5524  unixp0  5586  elsnxp  5594  iotauni  5780  iota1  5782  iota4  5786  dffv2  6181  fveqdmss  6262  eldmrexrnb  6274  exfo  6285  funop  6320  funsndifnop  6321  csbriota  6523  eusvobj2  6542  fnoprabg  6659  limuni3  6944  tfindsg  6952  findsg  6985  elxp5  7004  f1oexbi  7009  ffoss  7020  fo1stres  7083  fo2ndres  7084  eloprabi  7121  frxp  7174  suppimacnv  7193  mpt2xneldm  7225  mpt2xopxnop0  7228  reldmtpos  7247  dftpos4  7258  wfrlem2  7302  wfrlem3  7303  wfrlem4  7305  wfrdmcl  7310  wfrlem12  7313  tfrlem9  7368  ecdmn0  7676  mapprc  7748  ixpprc  7815  ixpn0  7826  bren  7850  brdomg  7851  ctex  7856  ener  7888  enerOLD  7889  en0  7905  en1  7909  en1b  7910  2dom  7915  fiprc  7924  pwdom  7997  domssex  8006  ssenen  8019  php  8029  isinf  8058  findcard2s  8086  hartogslem1  8330  brwdom  8355  brwdomn0  8357  wdompwdom  8366  unxpwdom2  8376  ixpiunwdom  8379  infeq5  8417  omex  8423  epfrs  8490  rankwflemb  8539  bnd2  8639  oncard  8669  carduni  8690  pm54.43  8709  ween  8741  acnrcl  8748  acndom  8757  acndom2  8760  iunfictbso  8820  aceq3lem  8826  dfac4  8828  dfac5lem4  8832  dfac5lem5  8833  dfac5  8834  dfac2a  8835  dfac2  8836  dfacacn  8846  dfac12r  8851  kmlem2  8856  kmlem16  8870  ackbij2  8948  cff  8953  cardcf  8957  cfeq0  8961  cfsuc  8962  cff1  8963  cfcoflem  8977  coftr  8978  infpssr  9013  fin4en1  9014  isfin4-2  9019  enfin2i  9026  fin23lem21  9044  fin23lem30  9047  fin23lem41  9057  enfin1ai  9089  fin1a2lem7  9111  domtriomlem  9147  axdc2lem  9153  axdc3lem2  9156  axdc4lem  9160  axcclem  9162  ac6s  9189  zorn2lem7  9207  ttukey2g  9221  axdc  9226  brdom3  9231  brdom5  9232  brdom4  9233  brdom7disj  9234  brdom6disj  9235  konigthlem  9269  pwcfsdom  9284  pwfseq  9365  tsk0  9464  gruina  9519  grothpw  9527  ltbtwnnq  9679  reclem2pr  9749  supsrlem  9811  supsr  9812  axpre-sup  9869  dedekindle  10080  nnunb  11165  ioorebas  12146  fzn0  12226  fzon0  12356  axdc4uzlem  12644  hasheqf1oi  13002  hasheqf1oiOLD  13003  hash1snb  13068  hashf1lem2  13097  hashge2el2difr  13118  hashge3el3dif  13122  fundmge2nop0  13129  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  swrdcl  13271  relexpindlem  13651  fclim  14132  climmo  14136  rlimdmo1  14196  xpsfrnel2  16048  cicsym  16287  cictr  16288  brssc  16297  sscpwex  16298  initoid  16478  termoid  16479  initoeu1  16484  initoeu2lem1  16487  initoeu2  16489  termoeu1  16491  opifismgm  17081  grpidval  17083  dfgrp3e  17338  subgint  17441  giclcl  17537  gicrcl  17538  gicsym  17539  gicen  17543  gicsubgen  17544  cntzssv  17584  giccyg  18124  brric2  18568  ricgic  18569  subrgint  18625  lmiclcl  18891  lmicrcl  18892  lmicsym  18893  abvn0b  19123  mpfrcl  19339  ply1frcl  19504  pf1rcl  19534  lmiclbs  19995  lmisfree  20000  lmictra  20003  mat1scmat  20164  neitr  20794  cmpsub  21013  bwth  21023  iuncon  21041  2ndcsb  21062  unisngl  21140  elpt  21185  ptclsg  21228  hmphsym  21395  hmphen  21398  haushmphlem  21400  cmphmph  21401  conhmph  21402  reghmph  21406  nrmhmph  21407  hmphdis  21409  indishmph  21411  hmphen2  21412  ufldom  21576  alexsubALTlem2  21662  alexsubALT  21665  metustfbas  22172  iunmbl2  23132  ioorcl2  23146  ioorinv2  23149  opnmblALT  23177  plyssc  23760  aannenlem2  23888  mulog2sum  25026  istrkg2ld  25159  axcontlem4  25647  usgraedg4  25916  edgusgranbfin  25979  uvtx01vtx  26020  3v3e3cycl2  26192  wlknwwlknsur  26240  wlkiswwlksur  26247  wwlknndef  26265  wlk0  26289  clwwlknndef  26301  2spontn0vne  26414  rusgrasn  26472  eupath  26508  vdfrgra0  26549  usgn0fidegnn0  26556  frgrawopreglem2  26572  friendship  26649  shintcli  27572  strlem1  28493  eqvincg  28698  rexunirn  28715  cnvoprab  28886  prsdm  29288  prsrn  29289  0elsiga  29504  sigaclcu  29507  issgon  29513  insiga  29527  omssubaddlem  29688  omssubadd  29689  bnj521  30059  bnj906  30254  bnj938  30261  bnj1018  30286  bnj1020  30287  bnj1125  30314  bnj1145  30315  mppspstlem  30722  frrlem2  31025  frrlem3  31026  frrlem4  31027  frrlem5e  31032  frrlem11  31036  txpss3v  31155  pprodss4v  31161  elsingles  31195  fnimage  31206  funpartlem  31219  funpartfun  31220  dfrdg4  31228  colinearex  31337  bj-sbex  31815  bj-cleljusti  31856  axc11n11r  31860  bj-eunex  31987  bj-mo3OLD  32022  bj-snglex  32154  bj-restpw  32226  bj-toprntopon  32244  bj-topnex  32247  mptsnunlem  32361  wl-sbcom2d  32523  wl-mo3t  32537  ptrecube  32579  mblfinlem3  32618  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  indexdom  32699  prtlem16  33172  sbccomieg  36375  setindtr  36609  setindtrs  36610  dfac11  36650  lnmlmic  36676  gicabl  36687  isnumbasgrplem1  36690  rtrclex  36943  clcnvlem  36949  brtrclfv2  37038  snhesn  37100  frege55b  37211  frege55c  37232  iotain  37640  iotavalb  37653  sbiota1  37657  iunconlem2  38193  fnchoice  38211  stoweidlem59  38952  vitali2  39585  nsssmfmbf  39665  pfxcl  40249  funop1  40327  hash1n0  40370  lfuhgr1v0e  40480  nbgr1vtx  40580  edgusgrnbfin  40601  cplgr1vlem  40651  cplgr1v  40652  fusgrn0degnn0  40714  g01wlk0  40860  wspthneq1eq2  41056  1wlkpwwlkf1ouspgr  41076  wlknwwlksnsur  41087  wlkwwlksur  41094  wwlksnndef  41111  wspthsnonn0vne  41124  clwwlksnndef  41198  eulerpath  41409  frgrwopreglem2  41482  av-friendship  41553  opmpt2ismgm  41597  nzerooringczr  41864  setrec1lem3  42235  elsetrecs  42244  elpglem1  42253