Theorem exlimiv 1960

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

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

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

Syntax hints:   → wi 4  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  exlimiiv  1961  exlimivv  1962  exsbim  2032  ax8  2149  ax9  2157  dfeumo  2564  mo3  2592  mo4  2594  moanimv  2647  euanv  2652  mopick  2653  clelab  2907  rexlimiva  3158  gencl  3496  cgsexg  3499  gencbvex2  3512  vtocleg  3521  eqvincg  3607  elrabi  3646  sbcex2  3804  sbccomlem  3822  eluni  4875  intab  4943  uniintsn  4950  dfiun2g  4994  disjiun  5097  trintss  5237  axrep6g  5251  sepexlem  5262  intex  5314  axpweq  5321  eunex  5361  eusvnf  5363  eusvnfb  5364  reusv2lem3  5371  axprglem  5407  axprg  5408  unipw  5431  moabex  5439  moabexOLD  5440  nnullss  5443  exss  5444  sbcop1  5470  mosubopt  5493  opelopabsb  5514  relop  5836  dmopab2rex  5907  dmrnssfld  5964  dmsnopg  6214  unixp0  6284  elsnxp  6292  iotauni2  6508  iotanul2  6509  iotaex  6512  iotauni  6513  iota1  6515  iota4  6517  dffv2  6976  fveqdmss  7073  eldmrexrnb  7087  exfo  7100  funop  7146  funopdmsn  7147  funsndifnop  7148  csbriota  7382  eusvobj2  7402  fnoprabg  7533  limuni3  7844  tfindsg  7853  findsg  7890  elxp5  7916  f1oexbi  7921  ffoss  7939  fo1stres  8008  fo2ndres  8009  eloprabi  8056  frxp  8118  suppimacnv  8166  mpoxneldm  8204  mpoxopxnop0  8207  reldmtpos  8226  dftpos4  8237  frrlem2  8280  frrlem3  8281  frrlem4  8282  frrlem8  8286  tfrlem9  8368  ecdmn0  8743  mapprc  8824  fsetprcnex  8855  ixpprc  8913  ixpn0  8924  bren  8949  brdomg  8951  domssl  8991  domssr  8992  ener  8994  en0  9011  en0ALT  9012  en0r  9013  en1  9017  en1b  9018  2dom  9023  fiprc  9037  dom0  9089  pwdom  9113  domssex  9122  ssenen  9135  dif1en  9142  findcard2s  9146  ensymfib  9164  php  9187  sdom1  9206  1sdom2dom  9210  isinf  9221  en1eqsn  9231  infn0  9258  pwfir  9272  fodomfir  9283  hartogslem1  9500  brwdom  9525  brwdomn0  9527  wdompwdom  9536  unxpwdom2  9546  ixpiunwdom  9548  elirrvOLD  9556  infeq5  9602  brttrcl  9678  ttrcltr  9681  dmttrcl  9686  rnttrcl  9687  epfrs  9696  rankwflemb  9761  bnd2  9875  oncard  9942  carduni  9963  pm54.43  9983  ween  10015  acnrcl  10022  acndom  10031  acndom2  10034  iunfictbso  10094  aceq3lem  10100  dfac4  10102  dfac5lem4  10106  dfac5lem5  10107  dfac5  10108  dfac2a  10109  dfac2b  10110  dfacacn  10121  dfac12r  10126  kmlem2  10131  kmlem16  10145  ackbij2  10221  cff  10226  cardcf  10230  cfeq0  10235  cfsuc  10236  cff1  10237  cfcoflem  10251  coftr  10252  infpssr  10287  fin4en1  10288  isfin4-2  10293  enfin2i  10300  fin23lem21  10318  fin23lem30  10321  fin23lem41  10331  enfin1ai  10363  fin1a2lem7  10385  domtriomlem  10421  axdc2lem  10427  axdc3lem2  10430  axdc4lem  10434  axcclem  10436  ac6s  10463  zorn2lem7  10481  ttukey2g  10495  axdc  10500  brdom3  10507  brdom5  10508  brdom4  10509  brdom7disj  10510  brdom6disj  10511  konigthlem  10548  pwfseq  10644  tsk0  10743  gruina  10798  ltbtwnnq  10958  reclem2pr  11028  supsrlem  11091  supsr  11092  axpre-sup  11149  dedekindle  11369  nnunb  12495  ioorebas  13473  fzn0  13561  fzon0  13702  axdc4uzlem  14015  hasheqf1oi  14383  hash1snb  14452  hash1n0  14454  hashf1lem2  14489  hashle2pr  14510  hashge2el2difr  14514  hashge3el3dif  14520  fi1uzind  14540  brfi1indALT  14543  swrdcl  14679  pfxcl  14711  relexpindlem  15096  fclim  15600  climmo  15604  rlimdmo1  15665  cicsym  17856  cictr  17857  brssc  17866  sscpwex  17867  initoid  18053  termoid  18054  initoeu1  18063  initoeu2lem1  18066  initoeu2  18068  termoeu1  18070  opifismgm  18712  grpidval  18714  dfgrp3e  19101  subgint  19212  giclcl  19338  gicrcl  19339  gicsym  19340  gicen  19343  gicsubgen  19344  cntzssv  19393  symgvalstruct  19462  giccyg  19965  riclcl  20597  ricrcl  20598  ricsym  20599  isbrric2  20601  ricgic  20603  subrngint  20659  subrgint  20694  abvn0b  20939  lmiclcl  21191  lmicrcl  21192  lmicsym  21193  nzerooringczr  21630  lmiclbs  21987  lmisfree  21992  lmictra  21995  mpfrcl  22236  ply1frcl  22478  pf1rcl  22509  mat1scmat  22696  toprntopon  23082  topnex  23153  neitr  23337  cmpsub  23557  bwth  23567  iunconn  23585  2ndcsb  23606  unisngl  23684  elpt  23729  ptclsg  23772  hmphsym  23939  hmphen  23942  haushmphlem  23944  cmphmph  23945  connhmph  23946  reghmph  23950  nrmhmph  23951  hmphdis  23953  indishmph  23955  hmphen2  23956  ufldom  24119  alexsubALTlem2  24205  alexsubALT  24208  metustfbas  24714  iunmbl2  25716  ioorcl2  25731  ioorinv2  25734  opnmblALT  25762  plyssc  26357  aannenlem2  26492  sltstr  27980  oncutlt  28457  istrkg2ld  28729  axcontlem4  29317  lfuhgr1v0e  29604  nbgr1vtx  29708  edgusgrnbfin  29723  cplgr1vlem  29779  cplgr1v  29780  fusgrn0degnn0  29849  g0wlk0  30000  wspthneq1eq2  30209  wlkswwlksf1o  30228  wwlksnndef  30254  wspthsnonn0vne  30266  eulerpath  30592  frgrwopreglem2  30664  friendship  30750  shintcli  31681  strlem1  32602  rexunirn  32838  iunrnmptss  32910  lsmsnorb  33704  mxidlnzrb  33762  prsdm  34304  prsrn  34305  0elsiga  34504  sigaclcu  34507  issgon  34513  insiga  34527  omssubaddlem  34689  omssubadd  34690  bnj906  35318  bnj938  35325  bnj1018g  35351  bnj1018  35352  bnj1020  35353  bnj1125  35380  bnj1145  35381  funen1cnv  35477  axprALT2  35503  rankscott  35522  rankscottu  35523  fineqvac  35529  fineqvnttrclselem1  35534  fineqvnttrclselem2  35535  onvf1odlem4  35590  vonf1oonfo  35599  lfuhgr3  35612  loop1cycl  35629  satfrnmapom  35862  satf0op  35869  sat1el2xp  35871  dmopab3rexdif  35897  mppspstlem  36063  txpss3v  36368  pprodss4v  36374  elsingles  36408  fnimage  36419  funpartlem  36434  funpartfun  36435  dfrdg4  36443  colinearex  36552  dfttc4  37041  ttcexg  37043  regsfromregtco  37049  bj-cleljusti  37302  axc11n11r  37308  bj-exlimvmpi  37546  bj-snglex  37609  bj-unexg  37674  bj-bm1.3ii  37700  bj-axseprep  37711  bj-restpw  37734  mptsnunlem  37984  ctbssinf  38052  pibt2  38063  wl-ax12v2cl  38152  wl-moteq  38169  wl-sbcom2d  38216  wl-mo3t  38231  ptrecube  38271  mblfinlem3  38310  ovoliunnfl  38313  voliunnfl  38315  volsupnfl  38316  indexdom  38385  xrnss3v  39030  prtlem16  39643  riccrng1  43289  ricdrng1  43296  sbccomieg  43520  setindtr  43751  setindtrs  43752  dfac11  43789  lnmlmic  43815  gicabl  43826  isnumbasgrplem1  43828  iscard4  44259  rtrclex  44343  clcnvlem  44349  brtrclfv2  44453  snhesn  44512  frege55b  44623  frege55c  44644  grucollcld  44970  grumnudlem  44995  iotain  45127  iotavalb  45140  sbiota1  45144  iunconnlem2  45643  permaxun  45720  permac8prim  45723  fnchoice  45749  stoweidlem59  46773  vitali2  47408  nsssmfmbf  47493  fsetprcnexALT  47799  funop1  48020  sbcpr  48270  gricen  48690  grlicsym  48778  grlictr  48780  grlicen  48782  gricgrlic  48783  usgrexmpl12ngric  48803  usgrexmpl12ngrlic  48804  opmpoismgm  48932  mo0sn  49594  mofmo  49625  mofeu  49626  f1mo  49631  eloprab1st2nd  49646  neircl  49683  sectrcl  49800  invrcl  49802  isorcl  49811  isoval2  49813  initc  49869  uobffth  49996  uobeqw  49997  fullthinc  50228  termco  50259  termcbasmo  50261  isinito3  50278  oppctermhom  50282  functermc  50286  termc2  50296  eufunclem  50299  eufunc  50300  euendfunc  50304  arweuthinc  50307  arweutermc  50308  discsntermlem  50348  rellan  50401  relran  50402  termolmd  50448  setrec1lem3  50467  elsetrecs  50478  elpglem1  50489