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

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

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

This inference, along with its many variants such as rexlimdv 3025, 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 1855 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 1885 and ax-8 1989. (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 1759 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
3 ax5e 1838 . 2 (∃𝑥𝜓𝜓)
42, 3syl 17 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  exlimiiv  1856  exlimivv  1857  equvinv  1956  equvinvOLD  1959  ax8  1993  ax9  2000  19.8aOLD  2050  sbcom2  2444  euex  2493  mo3  2506  mopick  2534  gencl  3225  cgsexg  3228  gencbvex2  3241  vtocleg  3269  eqvinc  3318  elrabi  3347  sbcex2  3473  eluni  4412  intab  4479  uniintsn  4486  disjiun  4613  trintss  4739  intex  4790  axpweq  4812  eunex  4829  eusvnf  4831  eusvnfb  4832  reusv2lem3  4841  unipw  4889  moabex  4898  nnullss  4901  exss  4902  mosubopt  4942  opelopabsb  4955  relop  5242  dmrnssfld  5354  dmsnopg  5575  unixp0  5638  elsnxp  5646  iotauni  5832  iota1  5834  iota4  5838  dffv2  6238  fveqdmss  6320  eldmrexrnb  6332  exfo  6343  funop  6379  funopdmsn  6380  funsndifnop  6381  csbriota  6588  eusvobj2  6608  fnoprabg  6726  limuni3  7014  tfindsg  7022  findsg  7055  elxp5  7073  f1oexbi  7078  ffoss  7089  fo1stres  7152  fo2ndres  7153  eloprabi  7192  frxp  7247  suppimacnv  7266  mpt2xneldm  7298  mpt2xopxnop0  7301  reldmtpos  7320  dftpos4  7331  wfrlem2  7375  wfrlem3  7376  wfrlem4  7378  wfrdmcl  7383  wfrlem12  7386  tfrlem9  7441  ecdmn0  7749  mapprc  7821  ixpprc  7889  ixpn0  7900  bren  7924  brdomg  7925  ctex  7930  ener  7962  enerOLD  7963  en0  7979  en1  7983  en1b  7984  2dom  7989  fiprc  7999  pwdom  8072  domssex  8081  ssenen  8094  php  8104  isinf  8133  findcard2s  8161  hartogslem1  8407  brwdom  8432  brwdomn0  8434  wdompwdom  8443  unxpwdom2  8453  ixpiunwdom  8456  infeq5  8494  omex  8500  epfrs  8567  rankwflemb  8616  bnd2  8716  oncard  8746  carduni  8767  pm54.43  8786  ween  8818  acnrcl  8825  acndom  8834  acndom2  8837  iunfictbso  8897  aceq3lem  8903  dfac4  8905  dfac5lem4  8909  dfac5lem5  8910  dfac5  8911  dfac2a  8912  dfac2  8913  dfacacn  8923  dfac12r  8928  kmlem2  8933  kmlem16  8947  ackbij2  9025  cff  9030  cardcf  9034  cfeq0  9038  cfsuc  9039  cff1  9040  cfcoflem  9054  coftr  9055  infpssr  9090  fin4en1  9091  isfin4-2  9096  enfin2i  9103  fin23lem21  9121  fin23lem30  9124  fin23lem41  9134  enfin1ai  9166  fin1a2lem7  9188  domtriomlem  9224  axdc2lem  9230  axdc3lem2  9233  axdc4lem  9237  axcclem  9239  ac6s  9266  zorn2lem7  9284  ttukey2g  9298  axdc  9303  brdom3  9310  brdom5  9311  brdom4  9312  brdom7disj  9313  brdom6disj  9314  konigthlem  9350  pwcfsdom  9365  pwfseq  9446  tsk0  9545  gruina  9600  grothpw  9608  ltbtwnnq  9760  reclem2pr  9830  supsrlem  9892  supsr  9893  axpre-sup  9950  dedekindle  10161  nnunb  11248  ioorebas  12233  fzn0  12313  fzon0  12444  axdc4uzlem  12738  hasheqf1oi  13096  hasheqf1oiOLD  13097  hash1snb  13163  hash1n0  13165  hashf1lem2  13194  hashle2pr  13213  hashge2el2difr  13217  hashge3el3dif  13222  fi1uzind  13234  brfi1indALT  13237  fi1uzindOLD  13240  brfi1indALTOLD  13243  swrdcl  13373  relexpindlem  13753  fclim  14234  climmo  14238  rlimdmo1  14298  xpsfrnel2  16165  cicsym  16404  cictr  16405  brssc  16414  sscpwex  16415  initoid  16595  termoid  16596  initoeu1  16601  initoeu2lem1  16604  initoeu2  16606  termoeu1  16608  opifismgm  17198  grpidval  17200  dfgrp3e  17455  subgint  17558  giclcl  17654  gicrcl  17655  gicsym  17656  gicen  17660  gicsubgen  17661  cntzssv  17701  giccyg  18241  brric2  18685  ricgic  18686  subrgint  18742  lmiclcl  19010  lmicrcl  19011  lmicsym  19012  abvn0b  19242  mpfrcl  19458  ply1frcl  19623  pf1rcl  19653  lmiclbs  20116  lmisfree  20121  lmictra  20124  mat1scmat  20285  toprntopon  20669  topnex  20740  neitr  20924  cmpsub  21143  bwth  21153  iunconn  21171  2ndcsb  21192  unisngl  21270  elpt  21315  ptclsg  21358  hmphsym  21525  hmphen  21528  haushmphlem  21530  cmphmph  21531  connhmph  21532  reghmph  21536  nrmhmph  21537  hmphdis  21539  indishmph  21541  hmphen2  21542  ufldom  21706  alexsubALTlem2  21792  alexsubALT  21795  metustfbas  22302  iunmbl2  23265  ioorcl2  23280  ioorinv2  23283  opnmblALT  23311  plyssc  23894  aannenlem2  24022  mulog2sum  25160  istrkg2ld  25293  axcontlem4  25781  lfuhgr1v0e  26073  nbgr1vtx  26175  edgusgrnbfin  26196  cplgr1vlem  26246  cplgr1v  26247  fusgrn0degnn0  26315  g0wlk0  26451  wspthneq1eq2  26648  wlkpwwlkf1ouspgr  26668  wlknwwlksnsur  26679  wlkwwlksur  26686  wwlksnndef  26703  wspthsnonn0vne  26716  clwwlksnndef  26791  eulerpath  27001  frgrwopreglem2  27074  friendship  27145  shintcli  28076  strlem1  28997  eqvincg  29202  rexunirn  29220  cnvoprab  29382  prsdm  29784  prsrn  29785  0elsiga  30000  sigaclcu  30003  issgon  30009  insiga  30023  omssubaddlem  30184  omssubadd  30185  bnj521  30566  bnj906  30761  bnj938  30768  bnj1018  30793  bnj1020  30794  bnj1125  30821  bnj1145  30822  mppspstlem  31229  frrlem2  31535  frrlem3  31536  frrlem4  31537  frrlem5e  31542  frrlem11  31546  txpss3v  31680  pprodss4v  31686  elsingles  31720  fnimage  31731  funpartlem  31744  funpartfun  31745  dfrdg4  31753  colinearex  31862  bj-sbex  32321  bj-cleljusti  32364  axc11n11r  32368  bj-eunex  32495  bj-mo3OLD  32530  bj-snglex  32661  bj-restpw  32735  mptsnunlem  32856  wl-sbcom2d  33015  wl-mo3t  33029  wl-ax8clv1  33049  wl-ax8clv2  33052  ptrecube  33080  mblfinlem3  33119  ovoliunnfl  33122  voliunnfl  33124  volsupnfl  33125  indexdom  33200  prtlem16  33673  sbccomieg  36876  setindtr  37110  setindtrs  37111  dfac11  37151  lnmlmic  37177  gicabl  37188  isnumbasgrplem1  37191  rtrclex  37444  clcnvlem  37450  brtrclfv2  37539  snhesn  37601  frege55b  37712  frege55c  37733  iotain  38139  iotavalb  38152  sbiota1  38156  iunconnlem2  38693  fnchoice  38710  stoweidlem59  39613  vitali2  40245  nsssmfmbf  40324  funop1  40629  pfxcl  40715  opmpt2ismgm  41125  nzerooringczr  41390  setrec1lem3  41759  elsetrecs  41768  elpglem1  41777
  Copyright terms: Public domain W3C validator