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

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

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

This inference, along with its many variants such as rexlimdv 3059, 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 1898 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 1945 and ax-8 2032. (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 1802 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
3 ax5e 1881 . 2 (∃𝑥𝜓𝜓)
42, 3syl 17 1 (∃𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ex 1745
This theorem is referenced by:  exlimiiv  1899  exlimivv  1900  equvinv  2003  ax8  2036  ax9  2043  sbcom2  2473  euex  2522  mo3  2536  mopick  2564  gencl  3266  cgsexg  3269  gencbvex2  3282  vtocleg  3310  eqvincg  3360  elrabi  3391  sbcex2  3519  eluni  4471  intab  4539  uniintsn  4546  disjiun  4672  trintss  4802  intex  4850  axpweq  4872  eunex  4889  eusvnf  4891  eusvnfb  4892  reusv2lem3  4901  unipw  4948  moabex  4957  nnullss  4960  exss  4961  mosubopt  5001  opelopabsb  5014  relop  5305  dmrnssfld  5416  dmsnopg  5642  unixp0  5707  elsnxp  5715  iotauni  5901  iota1  5903  iota4  5907  dffv2  6310  fveqdmss  6394  eldmrexrnb  6406  exfo  6417  funop  6454  funopdmsn  6455  funsndifnop  6456  csbriota  6663  eusvobj2  6683  fnoprabg  6803  limuni3  7094  tfindsg  7102  findsg  7135  elxp5  7153  f1oexbi  7158  ffoss  7169  fo1stres  7236  fo2ndres  7237  eloprabi  7277  frxp  7332  suppimacnv  7351  mpt2xneldm  7383  mpt2xopxnop0  7386  reldmtpos  7405  dftpos4  7416  wfrlem2  7460  wfrlem3  7461  wfrlem4  7463  wfrdmcl  7468  wfrlem12  7471  tfrlem9  7526  ecdmn0  7832  mapprc  7903  ixpprc  7971  ixpn0  7982  bren  8006  brdomg  8007  ctex  8012  ener  8044  en0  8060  en1  8064  en1b  8065  2dom  8070  fiprc  8080  pwdom  8153  domssex  8162  ssenen  8175  php  8185  isinf  8214  findcard2s  8242  hartogslem1  8488  brwdom  8513  brwdomn0  8515  wdompwdom  8524  unxpwdom2  8534  ixpiunwdom  8537  infeq5  8572  omex  8578  epfrs  8645  rankwflemb  8694  bnd2  8794  oncard  8824  carduni  8845  pm54.43  8864  ween  8896  acnrcl  8903  acndom  8912  acndom2  8915  iunfictbso  8975  aceq3lem  8981  dfac4  8983  dfac5lem4  8987  dfac5lem5  8988  dfac5  8989  dfac2a  8990  dfac2  8991  dfacacn  9001  dfac12r  9006  kmlem2  9011  kmlem16  9025  ackbij2  9103  cff  9108  cardcf  9112  cfeq0  9116  cfsuc  9117  cff1  9118  cfcoflem  9132  coftr  9133  infpssr  9168  fin4en1  9169  isfin4-2  9174  enfin2i  9181  fin23lem21  9199  fin23lem30  9202  fin23lem41  9212  enfin1ai  9244  fin1a2lem7  9266  domtriomlem  9302  axdc2lem  9308  axdc3lem2  9311  axdc4lem  9315  axcclem  9317  ac6s  9344  zorn2lem7  9362  ttukey2g  9376  axdc  9381  brdom3  9388  brdom5  9389  brdom4  9390  brdom7disj  9391  brdom6disj  9392  konigthlem  9428  pwcfsdom  9443  pwfseq  9524  tsk0  9623  gruina  9678  grothpw  9686  ltbtwnnq  9838  reclem2pr  9908  supsrlem  9970  supsr  9971  axpre-sup  10028  dedekindle  10239  nnunb  11326  ioorebas  12313  fzn0  12393  fzon0  12526  axdc4uzlem  12822  hasheqf1oi  13180  hash1snb  13245  hash1n0  13247  hashf1lem2  13278  hashle2pr  13297  hashge2el2difr  13301  hashge3el3dif  13306  fi1uzind  13317  brfi1indALT  13320  swrdcl  13464  relexpindlem  13847  fclim  14328  climmo  14332  rlimdmo1  14392  xpsfrnel2  16272  cicsym  16511  cictr  16512  brssc  16521  sscpwex  16522  initoid  16702  termoid  16703  initoeu1  16708  initoeu2lem1  16711  initoeu2  16713  termoeu1  16715  opifismgm  17305  grpidval  17307  dfgrp3e  17562  subgint  17665  giclcl  17761  gicrcl  17762  gicsym  17763  gicen  17766  gicsubgen  17767  cntzssv  17807  giccyg  18347  brric2  18793  ricgic  18794  subrgint  18850  lmiclcl  19118  lmicrcl  19119  lmicsym  19120  abvn0b  19350  mpfrcl  19566  ply1frcl  19731  pf1rcl  19761  lmiclbs  20224  lmisfree  20229  lmictra  20232  mat1scmat  20393  toprntopon  20777  topnex  20848  neitr  21032  cmpsub  21251  bwth  21261  iunconn  21279  2ndcsb  21300  unisngl  21378  elpt  21423  ptclsg  21466  hmphsym  21633  hmphen  21636  haushmphlem  21638  cmphmph  21639  connhmph  21640  reghmph  21644  nrmhmph  21645  hmphdis  21647  indishmph  21649  hmphen2  21650  ufldom  21813  alexsubALTlem2  21899  alexsubALT  21902  metustfbas  22409  iunmbl2  23371  ioorcl2  23386  ioorinv2  23389  opnmblALT  23417  plyssc  24001  aannenlem2  24129  mulog2sum  25271  istrkg2ld  25404  axcontlem4  25892  lfuhgr1v0e  26191  nbgr1vtx  26299  edgusgrnbfin  26319  cplgr1vlem  26381  cplgr1v  26382  fusgrn0degnn0  26451  g0wlk0  26604  wspthneq1eq2  26814  wlkpwwlkf1ouspgr  26833  wlknwwlksnsur  26844  wlkwwlksur  26851  wwlksnndef  26868  wspthsnonn0vne  26882  eulerpath  27219  frgrwopreglem2  27293  friendship  27386  shintcli  28316  strlem1  29237  rexunirn  29458  cnvoprabOLD  29626  prsdm  30088  prsrn  30089  0elsiga  30305  sigaclcu  30308  issgon  30314  insiga  30328  omssubaddlem  30489  omssubadd  30490  bnj521  30931  bnj906  31126  bnj938  31133  bnj1018  31158  bnj1020  31159  bnj1125  31186  bnj1145  31187  mppspstlem  31594  frrlem2  31906  frrlem3  31907  frrlem4  31908  frrlem5e  31913  frrlem11  31917  sslttr  32039  txpss3v  32110  pprodss4v  32116  elsingles  32150  fnimage  32161  funpartlem  32174  funpartfun  32175  dfrdg4  32183  colinearex  32292  bj-sbex  32751  bj-cleljusti  32794  axc11n11r  32798  bj-eunex  32924  bj-mo3OLD  32957  bj-snglex  33086  bj-restpw  33170  mptsnunlem  33315  wl-sbcom2d  33474  wl-mo3t  33488  wl-ax8clv1  33508  wl-ax8clv2  33511  ptrecube  33539  mblfinlem3  33578  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  indexdom  33659  xrnss3v  34274  prtlem16  34473  sbccomieg  37674  setindtr  37908  setindtrs  37909  dfac11  37949  lnmlmic  37975  gicabl  37986  isnumbasgrplem1  37988  rtrclex  38241  clcnvlem  38247  brtrclfv2  38336  snhesn  38397  frege55b  38508  frege55c  38529  iotain  38935  iotavalb  38948  sbiota1  38952  iunconnlem2  39485  fnchoice  39502  stoweidlem59  40594  vitali2  41229  nsssmfmbf  41308  funop1  41625  pfxcl  41711  opmpt2ismgm  42132  nzerooringczr  42397  setrec1lem3  42761  elsetrecs  42771  elpglem1  42782
  Copyright terms: Public domain W3C validator