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

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

This inference, along with our many variants such as rexlimdv 2829, 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.mathsci.appstate.edu/~hirstjl/primer/hirst.pdf.

In informal proofs, the statement "Let  C 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  x exists satisfying a wff, i.e.  E. x ph ( x ) where  ph ( x ) has  x free, then we can use  ph ( C ) as a hypothesis for the proof where  C is a new (ficticious) 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  ph (containing  x) as an antecedent for the main part of the proof. We eventually arrive at  ( ph  ->  ps ) where  ps is the theorem to be proved and does not contain  x. Then we apply exlimiv 1644 to arrive at  ( E. x ph  ->  ps ). Finally, we separately prove  E. x ph and detach it with modus ponens ax-mp 8 to arrive at the final theorem  ps. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 4-Dec-2017.)

Hypothesis
Ref Expression
exlimiv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
exlimiv  |-  ( E. x ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem exlimiv
StepHypRef Expression
1 exlimiv.1 . . 3  |-  ( ph  ->  ps )
21eximi 1585 . 2  |-  ( E. x ph  ->  E. x ps )
3 ax17e 1628 . 2  |-  ( E. x ps  ->  ps )
42, 3syl 16 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550
This theorem is referenced by:  exlimivv  1645  19.8a  1762  a9e  1952  ax12olem1OLD  2011  ax10  2025  equvin  2087  ax11vALT  2173  mo  2303  mopick  2343  gencl  2984  cgsexg  2987  gencbvex2  2999  vtocleg  3022  eqvinc  3063  elrabi  3090  sbcex2  3210  eluni  4018  intab  4080  uniintsn  4087  disjiun  4202  trint0  4319  bm1.3ii  4333  intex  4356  axpweq  4376  eunex  4392  unipw  4414  moabex  4422  nnullss  4425  exss  4426  mosubopt  4454  opelopabsb  4465  eusvnf  4718  eusvnfb  4719  reusv2lem3  4726  limuni3  4832  tfindsg  4840  findsg  4872  relop  5023  dmrnssfld  5129  dmsnopg  5341  elxp5  5358  unixp0  5403  iotauni  5430  iota1  5432  iota4  5436  ffoss  5707  dffv2  5796  eldmrexrnb  5877  exfo  5887  fnoprabg  6171  fo1stres  6370  fo2ndres  6371  eloprabi  6413  frxp  6456  mpt2xopxnop0  6466  reldmtpos  6487  dftpos4  6498  eusvobj2  6582  tfrlem9  6646  ecdmn0  6947  mapprc  7022  ixpprc  7083  ixpn0  7094  bren  7117  brdomg  7118  ener  7154  en0  7170  en1  7174  en1b  7175  2dom  7179  fiprc  7188  pwdom  7259  domssex  7268  ssenen  7281  php  7291  isinf  7322  findcard2s  7349  hartogslem1  7511  brwdom  7535  brwdomn0  7537  wdompwdom  7546  unxpwdom2  7556  ixpiunwdom  7559  inf3  7590  infeq5  7592  omex  7598  epfrs  7667  rankwflemb  7719  bnd2  7817  oncard  7847  carduni  7868  pm54.43  7887  ween  7916  acnrcl  7923  acndom  7932  acndom2  7935  iunfictbso  7995  aceq3lem  8001  dfac4  8003  dfac5lem4  8007  dfac5lem5  8008  dfac5  8009  dfac2a  8010  dfac2  8011  dfacacn  8021  dfac12r  8026  kmlem2  8031  kmlem16  8045  ackbij2  8123  cff  8128  cardcf  8132  cfeq0  8136  cfsuc  8137  cff1  8138  cfcoflem  8152  coftr  8153  infpssr  8188  fin4en1  8189  isfin4-2  8194  enfin2i  8201  fin23lem21  8219  fin23lem30  8222  fin23lem41  8232  enfin1ai  8264  fin1a2lem7  8286  axcc2lem  8316  domtriomlem  8322  dcomex  8327  axdc2lem  8328  axdc3lem2  8331  axdc4lem  8335  axcclem  8337  ac6s  8364  zorn2lem7  8382  ttukey2g  8396  axdclem2  8400  axdc  8401  brdom3  8406  brdom5  8407  brdom4  8408  brdom7disj  8409  brdom6disj  8410  konigthlem  8443  pwcfsdom  8458  pwfseq  8539  tsk0  8638  gruina  8693  grothpw  8701  grothpwex  8702  grothomex  8704  grothac  8705  ltbtwnnq  8855  reclem2pr  8925  supsrlem  8986  supsr  8987  axpre-sup  9044  nnunb  10217  ioorebas  11006  fzn0  11070  fzon0  11156  axdc4uzlem  11321  hasheqf1oi  11635  hash1snb  11681  hashf1lem2  11705  brfi1uzind  11715  swrdcl  11766  fclim  12347  climmo  12351  rlimdmo1  12411  cnso  12846  xpsfrnel2  13790  brssc  14014  sscpwex  14015  grpidval  14707  subgint  14964  giclcl  15059  gicrcl  15060  gicsym  15061  gicen  15064  gicsubgen  15065  cntzssv  15127  giccyg  15509  subrgint  15890  lmiclcl  16142  lmicrcl  16143  lmicsym  16144  abvn0b  16362  neitr  17244  cmpsub  17463  bwth  17473  iuncon  17491  2ndcsb  17512  elpt  17604  ptclsg  17647  hmphsym  17814  hmphen  17817  haushmphlem  17819  cmphmph  17820  conhmph  17821  reghmph  17825  nrmhmph  17826  hmphdis  17828  indishmph  17830  hmphen2  17831  ufldom  17994  alexsubALTlem2  18079  alexsubALT  18082  metustfbasOLD  18595  metustfbas  18596  iunmbl2  19451  ioorcl2  19464  ioorinv2  19467  opnmblALT  19495  mpfrcl  19939  pf1rcl  19969  plyssc  20119  aannenlem2  20246  aannenlem3  20247  mulog2sum  21231  usgraedg4  21406  edgusgranbfin  21459  uvtx01vtx  21501  3v3e3cycl2  21651  eupath  21703  shintcli  22831  strlem1  23753  eqvincg  23961  rexunirn  23978  ctex  24100  0elsiga  24497  sigaclcu  24500  issgon  24506  insiga  24520  relexpindlem  25139  dedekindle  25188  wfrlem2  25539  wfrlem3  25540  wfrlem4  25541  wfrlem9  25546  wfrlem12  25549  frrlem2  25583  frrlem3  25584  frrlem4  25585  frrlem5e  25590  frrlem11  25594  txpss3v  25723  pprodss4v  25729  elsingles  25763  fnimage  25774  funpartlem  25787  funpartfun  25788  dfrdg4  25795  axcontlem4  25906  colinearex  25994  mblfinlem3  26245  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  indexdom  26436  prtlem16  26718  sbccomieg  26849  setindtr  27095  setindtrs  27096  dfac11  27137  lnmlmic  27163  gicabl  27240  isnumbasgrplem1  27243  lmiclbs  27284  lmisfree  27289  iotain  27594  iotavalb  27607  sbiota1  27611  fnchoice  27676  stoweidlem59  27784  2spontn0vne  28354  vdfrgra0  28412  vdgfrgra0  28413  frgrawopreglem2  28434  iunconlem2  29047  bnj521  29104  bnj906  29301  bnj938  29308  bnj1018  29333  bnj1020  29334  bnj1125  29361  bnj1145  29362  equvinNEW7  29529
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator