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

Theorem exlimiv 1679
Description: Inference from Theorem 19.23 of [Margaris] p. 90, see 19.23 1834.

This inference, along with our many variants such as rexlimdv 2819, 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. 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 1679 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, 5-Aug-1993.) (Revised by Wolf Lammen to remove dependency on ax-6 and ax-8, 4-Dec-2017.)

Hypothesis
Ref Expression
exlimiv.1
Assertion
Ref Expression
exlimiv
Distinct variable group:   ,

Proof of Theorem exlimiv
StepHypRef Expression
1 exlimiv.1 . . 3
21eximi 1618 . 2
3 ax5e 1663 . 2
42, 3syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1581
This theorem is referenced by:  exlimivv  1680  equvin  1735  19.8a  1786  ax6e  1937  axc11n  1988  equvinOLD  2031  ax12vALT  2123  sbcom2  2143  euex  2269  mo3  2282  moOLD  2289  mopick  2325  mopickOLD  2326  gencl  2980  cgsexg  2983  gencbvex2  2995  vtocleg  3021  eqvinc  3064  elrabi  3092  sbcex2  3217  eluni  4069  intab  4133  uniintsn  4140  disjiun  4257  trint0  4377  bm1.3ii  4391  intex  4420  axpweq  4441  eunex  4457  eusvnf  4459  eusvnfb  4460  reusv2lem3  4467  unipw  4514  moabex  4523  nnullss  4526  exss  4527  mosubopt  4561  opelopabsb  4572  relop  4961  dmrnssfld  5069  dmsnopg  5282  unixp0  5343  iotauni  5365  iota1  5367  iota4  5371  dffv2  5734  eldmrexrnb  5820  exfo  5831  csbriota  6033  eusvobj2  6053  fnoprabg  6161  limuni3  6433  tfindsg  6441  findsg  6473  elxp5  6493  ffoss  6507  fo1stres  6569  fo2ndres  6570  eloprabi  6605  frxp  6651  suppimacnv  6670  mpt2xopxnop0  6694  reldmtpos  6715  dftpos4  6726  tfrlem9  6803  ecdmn0  7104  mapprc  7179  ixpprc  7243  ixpn0  7254  bren  7278  brdomg  7279  ener  7315  en0  7331  en1  7335  en1b  7336  2dom  7341  fiprc  7350  pwdom  7422  domssex  7431  ssenen  7444  php  7454  isinf  7485  findcard2s  7512  hartogslem1  7703  brwdom  7729  brwdomn0  7731  wdompwdom  7740  unxpwdom2  7750  ixpiunwdom  7753  inf3  7788  infeq5  7790  omex  7796  epfrs  7898  rankwflemb  7947  bnd2  8047  oncard  8077  carduni  8098  pm54.43  8117  ween  8152  acnrcl  8159  acndom  8168  acndom2  8171  iunfictbso  8231  aceq3lem  8237  dfac4  8239  dfac5lem4  8243  dfac5lem5  8244  dfac5  8245  dfac2a  8246  dfac2  8247  dfacacn  8257  dfac12r  8262  kmlem2  8267  kmlem16  8281  ackbij2  8359  cff  8364  cardcf  8368  cfeq0  8372  cfsuc  8373  cff1  8374  cfcoflem  8388  coftr  8389  infpssr  8424  fin4en1  8425  isfin4-2  8430  enfin2i  8437  fin23lem21  8455  fin23lem30  8458  fin23lem41  8468  enfin1ai  8500  fin1a2lem7  8522  axcc2lem  8552  domtriomlem  8558  dcomex  8563  axdc2lem  8564  axdc3lem2  8567  axdc4lem  8571  axcclem  8573  ac6s  8600  zorn2lem7  8618  ttukey2g  8632  axdclem2  8636  axdc  8637  brdom3  8642  brdom5  8643  brdom4  8644  brdom7disj  8645  brdom6disj  8646  konigthlem  8679  pwcfsdom  8694  pwfseq  8777  tsk0  8876  gruina  8931  grothpw  8939  grothpwex  8940  grothomex  8942  grothac  8943  ltbtwnnq  9093  reclem2pr  9163  supsrlem  9224  supsr  9225  axpre-sup  9282  dedekindle  9480  nnunb  10521  ioorebas  11336  fzn0  11408  fzon0  11510  axdc4uzlem  11745  hasheqf1oi  12063  hash1snb  12112  hashge3el3dif  12128  hashf1lem2  12150  brfi1uzind  12160  swrdcl  12256  fclim  12972  climmo  12976  rlimdmo1  13036  cnso  13469  xpsfrnel2  14443  brssc  14667  sscpwex  14668  grpidval  15372  subgint  15642  giclcl  15737  gicrcl  15738  gicsym  15739  gicen  15742  gicsubgen  15743  cntzssv  15783  giccyg  16312  subrgint  16700  lmiclcl  16960  lmicrcl  16961  lmicsym  16962  abvn0b  17182  lmiclbs  17965  lmisfree  17970  lmictra  17973  neitr  18488  cmpsub  18707  bwth  18717  bwthOLD  18718  iuncon  18736  2ndcsb  18757  elpt  18849  ptclsg  18892  hmphsym  19059  hmphen  19062  haushmphlem  19064  cmphmph  19065  conhmph  19066  reghmph  19070  nrmhmph  19071  hmphdis  19073  indishmph  19075  hmphen2  19076  ufldom  19239  alexsubALTlem2  19324  alexsubALT  19327  metustfbasOLD  19840  metustfbas  19841  iunmbl2  20738  ioorcl2  20752  ioorinv2  20755  opnmblALT  20783  mpfrcl  21227  pf1rcl  21257  plyssc  21409  aannenlem2  21536  aannenlem3  21537  mulog2sum  22527  tgldim0eq  22694  axcontlem4  22892  usgraedg4  22984  edgusgranbfin  23037  uvtx01vtx  23079  3v3e3cycl2  23229  eupath  23281  shintcli  24411  strlem1  25333  eqvincg  25538  rexunirn  25555  ctex  25688  cnvoprab  25703  prsdm  26053  prsrn  26054  0elsiga  26266  sigaclcu  26269  issgon  26275  insiga  26289  relexpindlem  27043  wfrlem2  27427  wfrlem3  27428  wfrlem4  27429  wfrlem9  27434  wfrlem12  27437  frrlem2  27471  frrlem3  27472  frrlem4  27473  frrlem5e  27478  frrlem11  27482  txpss3v  27611  pprodss4v  27617  elsingles  27651  fnimage  27662  funpartlem  27675  funpartfun  27676  dfrdg4  27683  colinearex  27793  mblfinlem3  28101  ovoliunnfl  28104  voliunnfl  28106  volsupnfl  28107  indexdom  28299  prtlem16  28686  sbccomieg  28804  setindtr  29046  setindtrs  29047  dfac11  29088  lnmlmic  29114  gicabl  29127  isnumbasgrplem1  29130  iotain  29344  iotavalb  29357  sbiota1  29361  fnchoice  29424  stoweidlem59  29528  f1oexbi  29830  wlk0  29966  wlknwwlknsur  30018  wlkiswwlksur  30025  wwlknndef  30043  2spontn0vne  30080  clwwlknndef  30110  rusgrasn  30231  vdfrgra0  30288  vdgfrgra0  30289  usgn0fidegnn0  30296  frgrawopreglem2  30312  friendship  30389  iunconlem2  31249  bnj521  31306  bnj906  31501  bnj938  31508  bnj1018  31533  bnj1020  31534  bnj1125  31561  bnj1145  31562  bj-axc11nv  31757  bj-snglex  31913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661
This theorem depends on definitions:  df-bi 179  df-ex 1582
  Copyright terms: Public domain W3C validator