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

Theorem exlimiv 1662
Description: Inference from Theorem 19.23 of [Margaris] p. 90.

This inference, along with our many variants such as rexlimdv 2883, 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 1662 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:   ,
Allowed substitution hint:   ( )

Proof of Theorem exlimiv
StepHypRef Expression
1 exlimiv.1 . . 3
21eximi 1602 . 2
3 ax5e 1646 . 2
42, 3syl 16 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  E.wex 1565
This theorem is referenced by:  exlimivv  1663  19.8a  1769  a6e  1959  axc9lem1OLD  2017  axc11n  2030  equvin  2095  ax12vALT  2190  sbcom2  2210  euex  2335  mo3  2344  moOLD  2352  mopick  2392  mopickOLD  2393  gencl  3043  cgsexg  3046  gencbvex2  3058  vtocleg  3083  eqvinc  3125  elrabi  3152  sbcex2  3277  eluni  4120  intab  4184  uniintsn  4191  disjiun  4308  trint0  4428  bm1.3ii  4442  intex  4471  axpweq  4492  eunex  4508  eusvnf  4510  eusvnfb  4511  reusv2lem3  4518  unipw  4565  moabex  4574  nnullss  4577  exss  4578  mosubopt  4611  opelopabsb  4622  relop  5012  dmrnssfld  5120  dmsnopg  5330  unixp0  5391  iotauni  5413  iota1  5415  iota4  5419  dffv2  5780  eldmrexrnb  5866  exfo  5877  csbriota  6075  eusvobj2  6095  fnoprabg  6203  limuni3  6473  tfindsg  6481  findsg  6513  elxp5  6531  ffoss  6545  fo1stres  6606  fo2ndres  6607  eloprabi  6642  frxp  6688  mpt2xopxnop0  6698  reldmtpos  6719  dftpos4  6730  tfrlem9  6808  ecdmn0  7109  mapprc  7184  ixpprc  7247  ixpn0  7258  bren  7281  brdomg  7282  ener  7318  en0  7334  en1  7338  en1b  7339  2dom  7344  fiprc  7353  pwdom  7424  domssex  7433  ssenen  7446  php  7456  isinf  7487  findcard2s  7514  hartogslem1  7678  brwdom  7702  brwdomn0  7704  wdompwdom  7713  unxpwdom2  7723  ixpiunwdom  7726  inf3  7757  infeq5  7759  omex  7765  epfrs  7834  rankwflemb  7886  bnd2  7986  oncard  8016  carduni  8037  pm54.43  8056  ween  8087  acnrcl  8094  acndom  8103  acndom2  8106  iunfictbso  8166  aceq3lem  8172  dfac4  8174  dfac5lem4  8178  dfac5lem5  8179  dfac5  8180  dfac2a  8181  dfac2  8182  dfacacn  8192  dfac12r  8197  kmlem2  8202  kmlem16  8216  ackbij2  8294  cff  8299  cardcf  8303  cfeq0  8307  cfsuc  8308  cff1  8309  cfcoflem  8323  coftr  8324  infpssr  8359  fin4en1  8360  isfin4-2  8365  enfin2i  8372  fin23lem21  8390  fin23lem30  8393  fin23lem41  8403  enfin1ai  8435  fin1a2lem7  8457  axcc2lem  8487  domtriomlem  8493  dcomex  8498  axdc2lem  8499  axdc3lem2  8502  axdc4lem  8506  axcclem  8508  ac6s  8535  zorn2lem7  8553  ttukey2g  8567  axdclem2  8571  axdc  8572  brdom3  8577  brdom5  8578  brdom4  8579  brdom7disj  8580  brdom6disj  8581  konigthlem  8614  pwcfsdom  8629  pwfseq  8710  tsk0  8809  gruina  8864  grothpw  8872  grothpwex  8873  grothomex  8875  grothac  8876  ltbtwnnq  9026  reclem2pr  9096  supsrlem  9157  supsr  9158  axpre-sup  9215  nnunb  10441  ioorebas  11254  fzn0  11320  fzon0  11421  axdc4uzlem  11653  hasheqf1oi  11971  hash1snb  12020  hashf1lem2  12056  brfi1uzind  12066  swrdcl  12162  fclim  12878  climmo  12882  rlimdmo1  12942  cnso  13376  xpsfrnel2  14344  brssc  14568  sscpwex  14569  grpidval  15273  subgint  15535  giclcl  15630  gicrcl  15631  gicsym  15632  gicen  15635  gicsubgen  15636  cntzssv  15736  giccyg  16119  subrgint  16506  lmiclcl  16765  lmicrcl  16766  lmicsym  16767  abvn0b  16987  neitr  18258  cmpsub  18477  bwth  18487  bwthOLD  18488  iuncon  18506  2ndcsb  18527  elpt  18619  ptclsg  18662  hmphsym  18829  hmphen  18832  haushmphlem  18834  cmphmph  18835  conhmph  18836  reghmph  18840  nrmhmph  18841  hmphdis  18843  indishmph  18845  hmphen2  18846  ufldom  19009  alexsubALTlem2  19094  alexsubALT  19097  metustfbasOLD  19610  metustfbas  19611  iunmbl2  20466  ioorcl2  20479  ioorinv2  20482  opnmblALT  20510  mpfrcl  20954  pf1rcl  20984  plyssc  21134  aannenlem2  21261  aannenlem3  21262  mulog2sum  22252  usgraedg4  22427  edgusgranbfin  22480  uvtx01vtx  22522  3v3e3cycl2  22672  eupath  22724  shintcli  23854  strlem1  24776  eqvincg  24986  rexunirn  25003  ctex  25138  cnvoprab  25153  prsdm  25523  prsrn  25524  0elsiga  25737  sigaclcu  25740  issgon  25746  insiga  25760  relexpindlem  26481  dedekindle  26527  wfrlem2  26878  wfrlem3  26879  wfrlem4  26880  wfrlem9  26885  wfrlem12  26888  frrlem2  26922  frrlem3  26923  frrlem4  26924  frrlem5e  26929  frrlem11  26933  txpss3v  27062  pprodss4v  27068  elsingles  27102  fnimage  27113  funpartlem  27126  funpartfun  27127  dfrdg4  27134  axcontlem4  27245  colinearex  27333  mblfinlem3  27610  ovoliunnfl  27613  voliunnfl  27615  volsupnfl  27616  indexdom  27808  prtlem16  28158  sbccomieg  28279  setindtr  28521  setindtrs  28522  dfac11  28563  lnmlmic  28589  gicabl  28603  isnumbasgrplem1  28606  lmiclbs  28647  lmisfree  28652  iotain  28845  iotavalb  28858  sbiota1  28862  fnchoice  28926  stoweidlem59  29033  f1oexbi  29337  wlk0  29473  wlknwwlknsur  29525  wlkiswwlksur  29532  wwlknndef  29550  2spontn0vne  29587  clwwlknndef  29617  rusgrasn  29738  vdfrgra0  29795  vdgfrgra0  29796  usgn0fidegnn0  29803  frgrawopreglem2  29819  friendship  29896  iunconlem2  30517  bnj521  30574  bnj906  30771  bnj938  30778  bnj1018  30803  bnj1020  30804  bnj1125  30831  bnj1145  30832  equvinNEW11  31081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644
This theorem depends on definitions:  df-bi 179  df-ex 1566
  Copyright terms: Public domain W3C validator