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

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

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

This inference, along with its many variants such as rexlimdv 3168, 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 2007 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 2054 and ax-8 2141. (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 1911 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
3 ax5e 1990 . 2 (∃𝑥𝜓𝜓)
42, 3syl 17 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988
This theorem depends on definitions:  df-bi 197  df-ex 1854
This theorem is referenced by:  exlimiiv  2008  exlimivv  2009  equvinv  2112  ax8  2145  ax9  2152  sbcom2  2582  euex  2631  mo3  2645  mopick  2673  gencl  3375  cgsexg  3378  gencbvex2  3391  vtocleg  3419  eqvincg  3468  elrabi  3499  sbcex2  3627  eluni  4591  intab  4659  uniintsn  4666  disjiun  4792  trintss  4921  intex  4969  axpweq  4991  eunex  5008  eusvnf  5010  eusvnfb  5011  reusv2lem3  5020  unipw  5067  moabex  5076  nnullss  5079  exss  5080  mosubopt  5120  opelopabsb  5135  relop  5428  dmrnssfld  5539  dmsnopg  5765  unixp0  5830  elsnxp  5838  iotauni  6024  iota1  6026  iota4  6030  dffv2  6433  fveqdmss  6517  eldmrexrnb  6529  exfo  6540  funop  6577  funopdmsn  6578  funsndifnop  6579  csbriota  6786  eusvobj2  6806  fnoprabg  6926  limuni3  7217  tfindsg  7225  findsg  7258  elxp5  7276  f1oexbi  7281  ffoss  7292  fo1stres  7359  fo2ndres  7360  eloprabi  7400  frxp  7455  suppimacnv  7474  mpt2xneldm  7507  mpt2xopxnop0  7510  reldmtpos  7529  dftpos4  7540  wfrlem2  7584  wfrlem3  7585  wfrlem4  7587  wfrdmcl  7592  wfrlem12  7595  tfrlem9  7650  ecdmn0  7956  mapprc  8027  ixpprc  8095  ixpn0  8106  bren  8130  brdomg  8131  ctex  8136  ener  8168  en0  8184  en1  8188  en1b  8189  2dom  8194  fiprc  8204  pwdom  8277  domssex  8286  ssenen  8299  php  8309  isinf  8338  findcard2s  8366  hartogslem1  8612  brwdom  8637  brwdomn0  8639  wdompwdom  8648  unxpwdom2  8658  ixpiunwdom  8661  infeq5  8707  omex  8713  epfrs  8780  rankwflemb  8829  bnd2  8929  oncard  8976  carduni  8997  pm54.43  9016  ween  9048  acnrcl  9055  acndom  9064  acndom2  9067  iunfictbso  9127  aceq3lem  9133  dfac4  9135  dfac5lem4  9139  dfac5lem5  9140  dfac5  9141  dfac2a  9142  dfac2b  9143  dfac2OLD  9145  dfacacn  9155  dfac12r  9160  kmlem2  9165  kmlem16  9179  ackbij2  9257  cff  9262  cardcf  9266  cfeq0  9270  cfsuc  9271  cff1  9272  cfcoflem  9286  coftr  9287  infpssr  9322  fin4en1  9323  isfin4-2  9328  enfin2i  9335  fin23lem21  9353  fin23lem30  9356  fin23lem41  9366  enfin1ai  9398  fin1a2lem7  9420  domtriomlem  9456  axdc2lem  9462  axdc3lem2  9465  axdc4lem  9469  axcclem  9471  ac6s  9498  zorn2lem7  9516  ttukey2g  9530  axdc  9535  brdom3  9542  brdom5  9543  brdom4  9544  brdom7disj  9545  brdom6disj  9546  konigthlem  9582  pwcfsdom  9597  pwfseq  9678  tsk0  9777  gruina  9832  grothpw  9840  ltbtwnnq  9992  reclem2pr  10062  supsrlem  10124  supsr  10125  axpre-sup  10182  dedekindle  10393  nnunb  11480  ioorebas  12468  fzn0  12548  fzon0  12681  axdc4uzlem  12976  hasheqf1oi  13334  hash1snb  13399  hash1n0  13401  hashf1lem2  13432  hashle2pr  13451  hashge2el2difr  13455  hashge3el3dif  13460  fi1uzind  13471  brfi1indALT  13474  swrdcl  13618  relexpindlem  14002  fclim  14483  climmo  14487  rlimdmo1  14547  xpsfrnel2  16427  cicsym  16665  cictr  16666  brssc  16675  sscpwex  16676  initoid  16856  termoid  16857  initoeu1  16862  initoeu2lem1  16865  initoeu2  16867  termoeu1  16869  opifismgm  17459  grpidval  17461  dfgrp3e  17716  subgint  17819  giclcl  17915  gicrcl  17916  gicsym  17917  gicen  17920  gicsubgen  17921  cntzssv  17961  giccyg  18501  brric2  18947  ricgic  18948  subrgint  19004  lmiclcl  19272  lmicrcl  19273  lmicsym  19274  abvn0b  19504  mpfrcl  19720  ply1frcl  19885  pf1rcl  19915  lmiclbs  20378  lmisfree  20383  lmictra  20386  mat1scmat  20547  toprntopon  20931  topnex  21002  neitr  21186  cmpsub  21405  bwth  21415  iunconn  21433  2ndcsb  21454  unisngl  21532  elpt  21577  ptclsg  21620  hmphsym  21787  hmphen  21790  haushmphlem  21792  cmphmph  21793  connhmph  21794  reghmph  21798  nrmhmph  21799  hmphdis  21801  indishmph  21803  hmphen2  21804  ufldom  21967  alexsubALTlem2  22053  alexsubALT  22056  metustfbas  22563  iunmbl2  23525  ioorcl2  23540  ioorinv2  23543  opnmblALT  23571  plyssc  24155  aannenlem2  24283  mulog2sum  25425  istrkg2ld  25558  axcontlem4  26046  lfuhgr1v0e  26345  nbgr1vtx  26453  edgusgrnbfin  26473  cplgr1vlem  26535  cplgr1v  26536  fusgrn0degnn0  26605  g0wlk0  26758  wspthneq1eq2  26969  wlkpwwlkf1ouspgr  26988  wlknwwlksnsur  26999  wlkwwlksur  27006  wwlksnndef  27023  wspthsnonn0vne  27037  eulerpath  27393  frgrwopreglem2  27467  friendship  27567  shintcli  28497  strlem1  29418  rexunirn  29639  cnvoprabOLD  29807  prsdm  30269  prsrn  30270  0elsiga  30486  sigaclcu  30489  issgon  30495  insiga  30509  omssubaddlem  30670  omssubadd  30671  bnj521  31112  bnj906  31307  bnj938  31314  bnj1018  31339  bnj1020  31340  bnj1125  31367  bnj1145  31368  mppspstlem  31775  frrlem2  32087  frrlem3  32088  frrlem4  32089  frrlem5e  32094  frrlem11  32098  sslttr  32220  txpss3v  32291  pprodss4v  32297  elsingles  32331  fnimage  32342  funpartlem  32355  funpartfun  32356  dfrdg4  32364  colinearex  32473  bj-sbex  32932  bj-cleljusti  32975  axc11n11r  32979  bj-eunex  33105  bj-mo3OLD  33138  bj-snglex  33267  bj-restpw  33351  mptsnunlem  33496  cnfinltrel  33552  wl-sbcom2d  33657  wl-mo3t  33671  wl-ax8clv1  33691  wl-ax8clv2  33694  ptrecube  33722  mblfinlem3  33761  ovoliunnfl  33764  voliunnfl  33766  volsupnfl  33767  indexdom  33842  xrnss3v  34457  prtlem16  34658  sbccomieg  37859  setindtr  38093  setindtrs  38094  dfac11  38134  lnmlmic  38160  gicabl  38171  isnumbasgrplem1  38173  rtrclex  38426  clcnvlem  38432  brtrclfv2  38521  snhesn  38582  frege55b  38693  frege55c  38714  iotain  39120  iotavalb  39133  sbiota1  39137  iunconnlem2  39670  fnchoice  39687  stoweidlem59  40779  vitali2  41414  nsssmfmbf  41493  funop1  41810  pfxcl  41896  opmpt2ismgm  42317  nzerooringczr  42582  setrec1lem3  42946  elsetrecs  42956  elpglem1  42967
  Copyright terms: Public domain W3C validator