MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimiv Structured version   Visualization version   GIF version

Theorem exlimiv 1934
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2205.

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

This inference, along with its many variants such as rexlimdv 3147, 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 3147. 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 1934 to arrive at (∃𝑥𝜑𝜓). Finally, we separately prove 𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1935. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1972 and ax-8 2109. (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
StepHypRef Expression
1 exlimiv.1 . . 3 (𝜑𝜓)
21eximi 1838 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
3 ax5e 1916 . 2 (∃𝑥𝜓𝜓)
42, 3syl 17 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  exlimiiv  1935  exlimivv  1936  exsbim  2006  ax8  2113  ax9  2121  dfeumo  2532  mo3  2559  mo4  2561  moanimv  2616  euanv  2621  mopick  2622  clelab  2880  rexlimiva  3141  gencl  3484  cgsexg  3487  ceqsexvOLD  3494  gencbvex2  3504  vtocleg  3513  vtoclgOLD  3525  eqvincg  3599  elrabi  3640  elrabiOLD  3641  sbcex2  3805  eluni  4869  intab  4940  uniintsn  4949  dfiun2g  4991  disjiun  5093  trintss  5242  axrep6g  5251  intex  5295  axpweq  5306  eunex  5346  eusvnf  5348  eusvnfb  5349  reusv2lem3  5356  unipw  5408  moabex  5417  nnullss  5420  exss  5421  sbcop1  5446  mosubopt  5468  opelopabsb  5488  relop  5807  dmopab2rex  5874  dmrnssfld  5926  dmsnopg  6166  unixp0  6236  elsnxp  6244  iotauni2  6466  iotanul2  6467  iotaex  6470  iotauni  6472  iota1  6474  iota4  6478  dffv2  6937  fveqdmss  7030  eldmrexrnb  7043  exfo  7056  funop  7096  funopdmsn  7097  funsndifnop  7098  csbriota  7330  eusvobj2  7350  fnoprabg  7480  limuni3  7789  tfindsg  7798  findsg  7837  elxp5  7861  f1oexbi  7866  ffoss  7879  fo1stres  7948  fo2ndres  7949  eloprabi  7996  frxp  8059  suppimacnv  8106  mpoxneldm  8144  mpoxopxnop0  8147  reldmtpos  8166  dftpos4  8177  frrlem2  8219  frrlem3  8220  frrlem4  8221  frrlem8  8225  wfrlem2OLD  8256  wfrlem3OLD  8257  wfrlem4OLD  8259  wfrdmclOLD  8264  wfrlem12OLD  8267  tfrlem9  8332  ecdmn0  8698  mapprc  8772  fsetprcnex  8803  ixpprc  8860  ixpn0  8871  bren  8896  brenOLD  8897  brdomg  8899  brdomgOLD  8900  domssl  8941  domssr  8942  ener  8944  en0  8960  en0OLD  8961  en0ALT  8962  en0r  8963  en1  8968  en1OLD  8969  en1b  8970  en1bOLD  8971  2dom  8977  fiprc  8992  dom0  9049  pwdom  9076  domssex  9085  ssenen  9098  rexdif1enOLD  9106  dif1en  9107  dif1enOLD  9109  findcard2s  9112  pwfir  9123  ensymfib  9134  php  9157  phpOLD  9169  sdom1  9189  1sdom2dom  9194  isinf  9207  isinfOLD  9208  en1eqsn  9221  infn0  9254  hartogslem1  9483  brwdom  9508  brwdomn0  9510  wdompwdom  9519  unxpwdom2  9529  ixpiunwdom  9531  infeq5  9578  omex  9584  brttrcl  9654  ttrcltr  9657  dmttrcl  9662  rnttrcl  9663  epfrs  9672  rankwflemb  9734  bnd2  9834  oncard  9901  carduni  9922  pm54.43  9942  ween  9976  acnrcl  9983  acndom  9992  acndom2  9995  iunfictbso  10055  aceq3lem  10061  dfac4  10063  dfac5lem4  10067  dfac5lem5  10068  dfac5  10069  dfac2a  10070  dfac2b  10071  dfacacn  10082  dfac12r  10087  kmlem2  10092  kmlem16  10106  ackbij2  10184  cff  10189  cardcf  10193  cfeq0  10197  cfsuc  10198  cff1  10199  cfcoflem  10213  coftr  10214  infpssr  10249  fin4en1  10250  isfin4-2  10255  enfin2i  10262  fin23lem21  10280  fin23lem30  10283  fin23lem41  10293  enfin1ai  10325  fin1a2lem7  10347  domtriomlem  10383  axdc2lem  10389  axdc3lem2  10392  axdc4lem  10396  axcclem  10398  ac6s  10425  zorn2lem7  10443  ttukey2g  10457  axdc  10462  brdom3  10469  brdom5  10470  brdom4  10471  brdom7disj  10472  brdom6disj  10473  konigthlem  10509  pwcfsdom  10524  pwfseq  10605  tsk0  10704  gruina  10759  ltbtwnnq  10919  reclem2pr  10989  supsrlem  11052  supsr  11053  axpre-sup  11110  dedekindle  11324  nnunb  12414  ioorebas  13374  fzn0  13461  fzon0  13596  axdc4uzlem  13894  hasheqf1oi  14257  hash1snb  14325  hash1n0  14327  hashf1lem2  14361  hashle2pr  14382  hashge2el2difr  14386  hashge3el3dif  14391  fi1uzind  14402  brfi1indALT  14405  swrdcl  14539  pfxcl  14571  relexpindlem  14954  fclim  15441  climmo  15445  rlimdmo1  15506  cicsym  17692  cictr  17693  brssc  17702  sscpwex  17703  initoid  17892  termoid  17893  initoeu1  17902  initoeu2lem1  17905  initoeu2  17907  termoeu1  17909  opifismgm  18519  grpidval  18521  dfgrp3e  18852  subgint  18957  giclcl  19067  gicrcl  19068  gicsym  19069  gicen  19072  gicsubgen  19073  cntzssv  19113  symgvalstruct  19183  symgvalstructOLD  19184  giccyg  19682  brric2  20186  ricgic  20187  subrgint  20258  lmiclcl  20546  lmicrcl  20547  lmicsym  20548  abvn0b  20788  lmiclbs  21259  lmisfree  21264  lmictra  21267  mpfrcl  21511  ply1frcl  21700  pf1rcl  21731  mat1scmat  21904  toprntopon  22290  topnex  22362  neitr  22547  cmpsub  22767  bwth  22777  iunconn  22795  2ndcsb  22816  unisngl  22894  elpt  22939  ptclsg  22982  hmphsym  23149  hmphen  23152  haushmphlem  23154  cmphmph  23155  connhmph  23156  reghmph  23160  nrmhmph  23161  hmphdis  23163  indishmph  23165  hmphen2  23166  ufldom  23329  alexsubALTlem2  23415  alexsubALT  23418  metustfbas  23929  iunmbl2  24937  ioorcl2  24952  ioorinv2  24955  opnmblALT  24983  plyssc  25577  aannenlem2  25705  mulog2sum  26901  sslttr  27168  istrkg2ld  27444  axcontlem4  27958  lfuhgr1v0e  28244  nbgr1vtx  28348  edgusgrnbfin  28363  cplgr1vlem  28419  cplgr1v  28420  fusgrn0degnn0  28489  g0wlk0  28642  wspthneq1eq2  28847  wlkswwlksf1o  28866  wwlksnndef  28892  wspthsnonn0vne  28904  eulerpath  29227  frgrwopreglem2  29299  friendship  29385  shintcli  30313  strlem1  31234  rexunirn  31463  iunrnmptss  31530  cnvoprabOLD  31684  lsmsnorb  32220  mxidlnzrb  32289  prsdm  32552  prsrn  32553  0elsiga  32770  sigaclcu  32773  issgon  32779  insiga  32793  omssubaddlem  32956  omssubadd  32957  bnj906  33599  bnj938  33606  bnj1018g  33632  bnj1018  33633  bnj1020  33634  bnj1125  33661  bnj1145  33662  funen1cnv  33749  fineqvac  33755  lfuhgr3  33770  loop1cycl  33788  satfrnmapom  34021  satf0op  34028  sat1el2xp  34030  dmopab3rexdif  34056  mppspstlem  34222  txpss3v  34509  pprodss4v  34515  elsingles  34549  fnimage  34560  funpartlem  34573  funpartfun  34574  dfrdg4  34582  colinearex  34691  bj-cleljusti  35190  axc11n11r  35194  bj-exlimvmpi  35424  bj-snglex  35490  bj-unexg  35555  bj-bm1.3ii  35581  bj-restpw  35609  mptsnunlem  35855  ctbssinf  35923  pibt2  35934  wl-moteq  36019  wl-sbcom2d  36062  wl-mo3t  36077  ptrecube  36124  mblfinlem3  36163  ovoliunnfl  36166  voliunnfl  36168  volsupnfl  36169  indexdom  36239  xrnss3v  36880  prtlem16  37377  ricsym  40746  riccrng1  40748  ricdrng1  40762  sbccomieg  41159  setindtr  41391  setindtrs  41392  dfac11  41432  lnmlmic  41458  gicabl  41469  isnumbasgrplem1  41471  iscard4  41893  rtrclex  41977  clcnvlem  41983  brtrclfv2  42087  snhesn  42146  frege55b  42257  frege55c  42278  grucollcld  42628  grumnudlem  42653  iotain  42785  iotavalb  42798  sbiota1  42802  iunconnlem2  43305  fnchoice  43322  stoweidlem59  44386  vitali2  45021  nsssmfmbf  45106  fsetprcnexALT  45382  funop1  45601  sbcpr  45799  opmpoismgm  46187  nzerooringczr  46456  mo0sn  46986  mofmo  46999  mofeu  47000  f1mo  47005  neircl  47023  fullthinc  47152  setrec1lem3  47220  elsetrecs  47231  elpglem1  47242
  Copyright terms: Public domain W3C validator