Theorem exlimiv 1930

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

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

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  exlimiiv  1931  exlimivv  1932  exsbim  2002  ax8  2115  ax9  2123  dfeumo  2530  mo3  2557  mo4  2559  moanimv  2612  euanv  2617  mopick  2618  clelab  2873  rexlimiva  3122  gencl  3480  cgsexg  3483  gencbvex2  3499  vtocleg  3510  vtoclgOLD  3528  eqvincg  3605  elrabi  3645  sbcex2  3805  sbccomlem  3823  eluni  4864  intab  4931  uniintsn  4938  dfiun2g  4983  disjiun  5083  trintss  5220  axrep6g  5232  sepexlem  5241  intex  5286  axpweq  5293  eunex  5332  eusvnf  5334  eusvnfb  5335  reusv2lem3  5342  unipw  5397  moabex  5406  nnullss  5409  exss  5410  sbcop1  5435  mosubopt  5457  opelopabsb  5477  relop  5797  dmopab2rex  5864  dmrnssfld  5919  dmsnopg  6166  unixp0  6235  elsnxp  6243  iotauni2  6458  iotanul2  6459  iotaex  6462  iotauni  6463  iota1  6465  iota4  6467  dffv2  6922  fveqdmss  7016  eldmrexrnb  7030  exfo  7043  funop  7087  funopdmsn  7088  funsndifnop  7089  csbriota  7325  eusvobj2  7345  fnoprabg  7476  limuni3  7792  tfindsg  7801  findsg  7837  elxp5  7863  f1oexbi  7868  ffoss  7888  fo1stres  7957  fo2ndres  7958  eloprabi  8005  frxp  8066  suppimacnv  8114  mpoxneldm  8152  mpoxopxnop0  8155  reldmtpos  8174  dftpos4  8185  frrlem2  8227  frrlem3  8228  frrlem4  8229  frrlem8  8233  tfrlem9  8314  ecdmn0  8684  mapprc  8764  fsetprcnex  8796  ixpprc  8853  ixpn0  8864  bren  8889  brdomg  8891  domssl  8930  domssr  8931  ener  8933  en0  8950  en0ALT  8951  en0r  8952  en1  8956  en1b  8957  2dom  8962  fiprc  8977  dom0  9029  pwdom  9053  domssex  9062  ssenen  9075  rexdif1enOLD  9083  dif1en  9084  dif1enOLD  9086  findcard2s  9089  ensymfib  9108  php  9131  sdom1  9149  1sdom2dom  9153  isinf  9165  isinfOLD  9166  en1eqsn  9177  infn0  9209  pwfir  9224  fodomfir  9237  hartogslem1  9453  brwdom  9478  brwdomn0  9480  wdompwdom  9489  unxpwdom2  9499  ixpiunwdom  9501  elirrv  9508  infeq5  9552  brttrcl  9628  ttrcltr  9631  dmttrcl  9636  rnttrcl  9637  epfrs  9646  rankwflemb  9708  bnd2  9808  oncard  9875  carduni  9896  pm54.43  9916  ween  9948  acnrcl  9955  acndom  9964  acndom2  9967  iunfictbso  10027  aceq3lem  10033  dfac4  10035  dfac5lem4  10039  dfac5lem5  10040  dfac5lem4OLD  10041  dfac5  10042  dfac2a  10043  dfac2b  10044  dfacacn  10055  dfac12r  10060  kmlem2  10065  kmlem16  10079  ackbij2  10155  cff  10161  cardcf  10165  cfeq0  10169  cfsuc  10170  cff1  10171  cfcoflem  10185  coftr  10186  infpssr  10221  fin4en1  10222  isfin4-2  10227  enfin2i  10234  fin23lem21  10252  fin23lem30  10255  fin23lem41  10265  enfin1ai  10297  fin1a2lem7  10319  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  axdc4lem  10368  axcclem  10370  ac6s  10397  zorn2lem7  10415  ttukey2g  10429  axdc  10434  brdom3  10441  brdom5  10442  brdom4  10443  brdom7disj  10444  brdom6disj  10445  konigthlem  10481  pwfseq  10577  tsk0  10676  gruina  10731  ltbtwnnq  10891  reclem2pr  10961  supsrlem  11024  supsr  11025  axpre-sup  11082  dedekindle  11298  nnunb  12398  ioorebas  13372  fzn0  13459  fzon0  13598  axdc4uzlem  13908  hasheqf1oi  14276  hash1snb  14344  hash1n0  14346  hashf1lem2  14381  hashle2pr  14402  hashge2el2difr  14406  hashge3el3dif  14412  fi1uzind  14432  brfi1indALT  14435  swrdcl  14570  pfxcl  14602  relexpindlem  14988  fclim  15478  climmo  15482  rlimdmo1  15543  cicsym  17729  cictr  17730  brssc  17739  sscpwex  17740  initoid  17926  termoid  17927  initoeu1  17936  initoeu2lem1  17939  initoeu2  17941  termoeu1  17943  opifismgm  18551  grpidval  18553  dfgrp3e  18937  subgint  19047  giclcl  19170  gicrcl  19171  gicsym  19172  gicen  19175  gicsubgen  19176  cntzssv  19225  symgvalstruct  19294  giccyg  19797  brric2  20409  ricgic  20410  subrngint  20463  subrgint  20498  abvn0b  20739  lmiclcl  20992  lmicrcl  20993  lmicsym  20994  nzerooringczr  21405  lmiclbs  21762  lmisfree  21767  lmictra  21770  mpfrcl  22008  ply1frcl  22221  pf1rcl  22252  mat1scmat  22442  toprntopon  22828  topnex  22899  neitr  23083  cmpsub  23303  bwth  23313  iunconn  23331  2ndcsb  23352  unisngl  23430  elpt  23475  ptclsg  23518  hmphsym  23685  hmphen  23688  haushmphlem  23690  cmphmph  23691  connhmph  23692  reghmph  23696  nrmhmph  23697  hmphdis  23699  indishmph  23701  hmphen2  23702  ufldom  23865  alexsubALTlem2  23951  alexsubALT  23954  metustfbas  24461  iunmbl2  25474  ioorcl2  25489  ioorinv2  25492  opnmblALT  25520  plyssc  26121  aannenlem2  26253  sslttr  27736  onscutlt  28188  istrkg2ld  28423  axcontlem4  28930  lfuhgr1v0e  29217  nbgr1vtx  29321  edgusgrnbfin  29336  cplgr1vlem  29392  cplgr1v  29393  fusgrn0degnn0  29463  g0wlk0  29614  wspthneq1eq2  29823  wlkswwlksf1o  29842  wwlksnndef  29868  wspthsnonn0vne  29880  eulerpath  30203  frgrwopreglem2  30275  friendship  30361  shintcli  31291  strlem1  32212  rexunirn  32454  iunrnmptss  32527  lsmsnorb  33341  mxidlnzrb  33430  prsdm  33883  prsrn  33884  0elsiga  34083  sigaclcu  34086  issgon  34092  insiga  34106  omssubaddlem  34269  omssubadd  34270  bnj906  34899  bnj938  34906  bnj1018g  34932  bnj1018  34933  bnj1020  34934  bnj1125  34961  bnj1145  34962  funen1cnv  35057  fineqvac  35074  onvf1odlem4  35081  lfuhgr3  35095  loop1cycl  35112  satfrnmapom  35345  satf0op  35352  sat1el2xp  35354  dmopab3rexdif  35380  mppspstlem  35546  txpss3v  35854  pprodss4v  35860  elsingles  35894  fnimage  35905  funpartlem  35918  funpartfun  35919  dfrdg4  35927  colinearex  36036  bj-cleljusti  36655  axc11n11r  36659  bj-exlimvmpi  36887  bj-snglex  36949  bj-unexg  37014  bj-bm1.3ii  37040  bj-restpw  37068  mptsnunlem  37314  ctbssinf  37382  pibt2  37393  wl-ax12v2cl  37482  wl-moteq  37490  wl-sbcom2d  37537  wl-mo3t  37552  ptrecube  37602  mblfinlem3  37641  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  indexdom  37716  xrnss3v  38342  prtlem16  38850  ricsym  42495  riccrng1  42497  ricdrng1  42504  sbccomieg  42769  setindtr  43000  setindtrs  43001  dfac11  43038  lnmlmic  43064  gicabl  43075  isnumbasgrplem1  43077  iscard4  43509  rtrclex  43593  clcnvlem  43599  brtrclfv2  43703  snhesn  43762  frege55b  43873  frege55c  43894  grucollcld  44236  grumnudlem  44261  iotain  44393  iotavalb  44406  sbiota1  44410  iunconnlem2  44911  permaxun  44988  permac8prim  44991  fnchoice  45010  stoweidlem59  46044  vitali2  46679  nsssmfmbf  46764  fsetprcnexALT  47050  funop1  47271  sbcpr  47509  gricen  47913  grlicsym  48001  grlictr  48003  grlicen  48005  gricgrlic  48006  usgrexmpl12ngric  48026  usgrexmpl12ngrlic  48027  opmpoismgm  48155  mo0sn  48804  mofmo  48835  mofeu  48836  f1mo  48841  eloprab1st2nd  48856  neircl  48893  sectrcl  49011  invrcl  49013  isorcl  49022  isoval2  49024  initc  49080  uobffth  49207  uobeqw  49208  fullthinc  49439  termco  49470  termcbasmo  49472  isinito3  49489  oppctermhom  49493  functermc  49497  termc2  49507  eufunclem  49510  eufunc  49511  euendfunc  49515  arweuthinc  49518  arweutermc  49519  discsntermlem  49559  rellan  49612  relran  49613  termolmd  49659  setrec1lem3  49678  elsetrecs  49689  elpglem1  49700