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

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

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

This inference, along with its many variants such as rexlimdv 3288, 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 3288. 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 1924 to arrive at (∃𝑥𝜑𝜓). Finally, we separately prove 𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1925. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1963 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 1828 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
3 ax5e 1906 . 2 (∃𝑥𝜓𝜓)
42, 3syl 17 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-ex 1774
This theorem is referenced by:  exlimiiv  1925  exlimivv  1926  exsbim  2001  spsbeOLD  2082  ax8  2113  ax9  2121  dfeumo  2617  mo3  2646  mo4  2648  moanimv  2703  euanv  2708  mopick  2709  gencl  3540  cgsexg  3543  gencbvex2  3556  vtocleg  3586  eqvincg  3645  elrabi  3679  sbcex2  3838  eluni  4840  intab  4904  uniintsn  4911  disjiun  5050  trintss  5186  intex  5237  axpweq  5262  eunex  5287  eusvnf  5289  eusvnfb  5290  reusv2lem3  5297  unipw  5339  moabex  5348  nnullss  5351  exss  5352  sbcop1  5376  mosubopt  5397  opelopabsb  5414  relop  5720  dmopab2rex  5785  dmrnssfld  5840  dmsnopg  6069  unixp0  6133  elsnxp  6141  iotauni  6329  iota1  6331  iota4  6335  dffv2  6755  fveqdmss  6844  eldmrexrnb  6856  exfo  6869  funop  6909  funopdmsn  6910  funsndifnop  6911  csbriota  7123  eusvobj2  7143  fnoprabg  7269  limuni3  7560  tfindsg  7568  findsg  7602  elxp5  7621  f1oexbi  7626  ffoss  7643  fo1stres  7711  fo2ndres  7712  eloprabi  7757  frxp  7816  suppimacnv  7837  mpoxneldm  7874  mpoxopxnop0  7877  reldmtpos  7896  dftpos4  7907  wfrlem2  7951  wfrlem3  7952  wfrlem4  7954  wfrdmcl  7959  wfrlem12  7962  tfrlem9  8017  ecdmn0  8331  mapprc  8405  ixpprc  8477  ixpn0  8488  bren  8512  brdomg  8513  ener  8550  en0  8566  en1  8570  en1b  8571  2dom  8576  fiprc  8589  pwdom  8663  domssex  8672  ssenen  8685  php  8695  isinf  8725  findcard2s  8753  hartogslem1  9000  brwdom  9025  brwdomn0  9027  wdompwdom  9036  unxpwdom2  9046  ixpiunwdom  9049  infeq5  9094  omex  9100  epfrs  9167  rankwflemb  9216  bnd2  9316  oncard  9383  carduni  9404  pm54.43  9423  ween  9455  acnrcl  9462  acndom  9471  acndom2  9474  iunfictbso  9534  aceq3lem  9540  dfac4  9542  dfac5lem4  9546  dfac5lem5  9547  dfac5  9548  dfac2a  9549  dfac2b  9550  dfacacn  9561  dfac12r  9566  kmlem2  9571  kmlem16  9585  ackbij2  9659  cff  9664  cardcf  9668  cfeq0  9672  cfsuc  9673  cff1  9674  cfcoflem  9688  coftr  9689  infpssr  9724  fin4en1  9725  isfin4-2  9730  enfin2i  9737  fin23lem21  9755  fin23lem30  9758  fin23lem41  9768  enfin1ai  9800  fin1a2lem7  9822  domtriomlem  9858  axdc2lem  9864  axdc3lem2  9867  axdc4lem  9871  axcclem  9873  ac6s  9900  zorn2lem7  9918  ttukey2g  9932  axdc  9937  brdom3  9944  brdom5  9945  brdom4  9946  brdom7disj  9947  brdom6disj  9948  konigthlem  9984  pwcfsdom  9999  pwfseq  10080  tsk0  10179  gruina  10234  ltbtwnnq  10394  reclem2pr  10464  supsrlem  10527  supsr  10528  axpre-sup  10585  dedekindle  10798  nnunb  11887  ioorebas  12834  fzn0  12916  fzon0  13050  axdc4uzlem  13346  hasheqf1oi  13707  hash1snb  13775  hash1n0  13777  hashf1lem2  13809  hashle2pr  13830  hashge2el2difr  13834  hashge3el3dif  13839  fi1uzind  13850  brfi1indALT  13853  swrdcl  14002  pfxcl  14034  relexpindlem  14417  fclim  14905  climmo  14909  rlimdmo1  14969  cicsym  17069  cictr  17070  brssc  17079  sscpwex  17080  initoid  17260  termoid  17261  initoeu1  17266  initoeu2lem1  17269  initoeu2  17271  termoeu1  17273  opifismgm  17864  grpidval  17866  dfgrp3e  18144  subgint  18248  giclcl  18357  gicrcl  18358  gicsym  18359  gicen  18362  gicsubgen  18363  cntzssv  18403  giccyg  18956  brric2  19436  ricgic  19437  subrgint  19493  lmiclcl  19778  lmicrcl  19779  lmicsym  19780  abvn0b  20010  mpfrcl  20233  ply1frcl  20416  pf1rcl  20447  lmiclbs  20916  lmisfree  20921  lmictra  20924  mat1scmat  21083  toprntopon  21468  topnex  21539  neitr  21723  cmpsub  21943  bwth  21953  iunconn  21971  2ndcsb  21992  unisngl  22070  elpt  22115  ptclsg  22158  hmphsym  22325  hmphen  22328  haushmphlem  22330  cmphmph  22331  connhmph  22332  reghmph  22336  nrmhmph  22337  hmphdis  22339  indishmph  22341  hmphen2  22342  ufldom  22505  alexsubALTlem2  22591  alexsubALT  22594  metustfbas  23101  iunmbl2  24092  ioorcl2  24107  ioorinv2  24110  opnmblALT  24138  plyssc  24724  aannenlem2  24852  mulog2sum  26046  istrkg2ld  26179  axcontlem4  26686  lfuhgr1v0e  26969  nbgr1vtx  27073  edgusgrnbfin  27088  cplgr1vlem  27144  cplgr1v  27145  fusgrn0degnn0  27214  g0wlk0  27366  wspthneq1eq2  27571  wlkswwlksf1o  27590  wwlksnndef  27616  wspthsnonn0vne  27629  eulerpath  27953  frgrwopreglem2  28025  friendship  28111  shintcli  29039  strlem1  29960  rexunirn  30189  iunrnmptss  30251  cnvoprabOLD  30388  prsdm  31062  prsrn  31063  0elsiga  31278  sigaclcu  31281  issgon  31287  insiga  31301  omssubaddlem  31462  omssubadd  31463  bnj521  31912  bnj906  32107  bnj938  32114  bnj1018  32139  bnj1020  32140  bnj1125  32167  bnj1145  32168  funen1cnv  32260  lfuhgr3  32269  loop1cycl  32287  satfrnmapom  32520  satf0op  32527  sat1el2xp  32529  dmopab3rexdif  32555  mppspstlem  32721  frrlem2  33027  frrlem3  33028  frrlem4  33029  frrlem8  33033  sslttr  33171  txpss3v  33242  pprodss4v  33248  elsingles  33282  fnimage  33293  funpartlem  33306  funpartfun  33307  dfrdg4  33315  colinearex  33424  bj-cleljusti  33916  axc11n11r  33920  bj-exlimvmpi  34130  bj-snglex  34188  bj-bm1.3ii  34257  bj-restpw  34283  mptsnunlem  34507  ctbssinf  34575  pibt2  34586  wl-moteq  34642  wl-sbcom2d  34683  wl-mo3t  34698  ptrecube  34778  mblfinlem3  34817  ovoliunnfl  34820  voliunnfl  34822  volsupnfl  34823  indexdom  34896  xrnss3v  35510  prtlem16  35891  sbccomieg  39274  setindtr  39505  setindtrs  39506  dfac11  39546  lnmlmic  39572  gicabl  39583  isnumbasgrplem1  39585  iscard4  39784  rtrclex  39861  clcnvlem  39867  brtrclfv2  39956  snhesn  40016  frege55b  40127  frege55c  40148  grucollcld  40480  grumnudlem  40505  iotain  40633  iotavalb  40646  sbiota1  40650  iunconnlem2  41153  fnchoice  41170  stoweidlem59  42229  vitali2  42861  nsssmfmbf  42940  funop1  43367  sbcpr  43534  opmpoismgm  43925  nzerooringczr  44245  setrec1lem3  44694  elsetrecs  44704  elpglem1  44715
  Copyright terms: Public domain W3C validator