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

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

This inference, along with our many variants such as rexlimdv 2742, 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 1634 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 1576 . 2  |-  ( E. x ph  ->  E. x ps )
3 ax17e 1618 . 2  |-  ( E. x ps  ->  ps )
42, 3syl 15 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1541
This theorem is referenced by:  exlimivv  1635  19.8a  1747  ax12olem1  1932  equvin  2006  ax11vALT  2102  mo  2231  mopick  2271  gencl  2892  cgsexg  2895  gencbvex2  2907  vtocleg  2930  eqvinc  2971  sbcex2  3116  eluni  3909  intab  3971  uniintsn  3978  disjiun  4092  trint0  4209  bm1.3ii  4223  intex  4246  axpweq  4266  eunex  4282  unipw  4303  moabex  4311  nnullss  4314  exss  4315  mosubopt  4343  opelopabsb  4354  eusvnf  4608  eusvnfb  4609  reusv2lem3  4616  limuni3  4722  tfindsg  4730  findsg  4762  relop  4913  dmrnssfld  5017  dmsnopg  5223  elxp5  5240  unixp0  5285  iotauni  5310  iota1  5312  iota4  5316  ffoss  5585  dffv2  5672  exfo  5758  fnoprabg  6029  fo1stres  6227  fo2ndres  6228  eloprabi  6270  frxp  6309  reldmtpos  6326  dftpos4  6337  eusvobj2  6421  tfrlem9  6485  ecdmn0  6786  mapprc  6861  ixpprc  6922  ixpn0  6933  bren  6956  brdomg  6957  ener  6993  en0  7009  en1  7013  en1b  7014  2dom  7018  fiprc  7027  pwdom  7098  domssex  7107  ssenen  7120  php  7130  isinf  7161  findcard2s  7186  hartogslem1  7344  brwdom  7368  brwdomn0  7370  wdompwdom  7379  unxpwdom2  7389  ixpiunwdom  7392  inf3  7423  infeq5  7425  omex  7431  epfrs  7500  rankwflemb  7552  bnd2  7650  oncard  7680  carduni  7701  pm54.43  7720  ween  7749  acnrcl  7756  acndom  7765  acndom2  7768  iunfictbso  7828  aceq3lem  7834  dfac4  7836  dfac5lem4  7840  dfac5lem5  7841  dfac5  7842  dfac2a  7843  dfac2  7844  dfacacn  7854  dfac12r  7859  kmlem2  7864  kmlem16  7878  ackbij2  7956  cff  7961  cardcf  7965  cfeq0  7969  cfsuc  7970  cff1  7971  cfcoflem  7985  coftr  7986  infpssr  8021  fin4en1  8022  isfin4-2  8027  enfin2i  8034  fin23lem21  8052  fin23lem30  8055  fin23lem41  8065  enfin1ai  8097  fin1a2lem7  8119  axcc2lem  8149  domtriomlem  8155  dcomex  8160  axdc2lem  8161  axdc3lem2  8164  axdc4lem  8168  axcclem  8170  ac6s  8198  zorn2lem7  8216  ttukey2g  8230  axdclem2  8234  axdc  8235  brdom3  8240  brdom5  8241  brdom4  8242  brdom7disj  8243  brdom6disj  8244  konigthlem  8277  pwcfsdom  8292  pwfseq  8373  tsk0  8472  gruina  8527  grothpw  8535  grothpwex  8536  grothomex  8538  grothac  8539  ltbtwnnq  8689  reclem2pr  8759  supsrlem  8820  supsr  8821  axpre-sup  8878  nnunb  10050  ioorebas  10834  fzn0  10898  fzon0  10980  axdc4uzlem  11133  hashf1lem2  11484  swrdcl  11542  fclim  12117  climmo  12121  rlimdmo1  12181  cnso  12616  xpsfrnel2  13560  brssc  13784  sscpwex  13785  grpidval  14477  subgint  14734  giclcl  14829  gicrcl  14830  gicsym  14831  gicen  14834  gicsubgen  14835  cntzssv  14897  giccyg  15279  subrgint  15660  lmiclcl  15916  lmicrcl  15917  lmicsym  15918  abvn0b  16136  cmpsub  17227  iuncon  17254  2ndcsb  17275  elpt  17367  ptclsg  17409  hmphsym  17573  hmphen  17576  haushmphlem  17578  cmphmph  17579  conhmph  17580  reghmph  17584  nrmhmph  17585  hmphdis  17587  indishmph  17589  hmphen2  17590  ufldom  17753  alexsubALTlem2  17838  alexsubALT  17841  iunmbl2  19012  ioorcl2  19025  ioorinv2  19028  opnmblALT  19056  mpfrcl  19500  pf1rcl  19530  plyssc  19680  aannenlem2  19807  aannenlem3  19808  mulog2sum  20792  shintcli  22016  strlem1  22938  eqvincg  23144  rexunirn  23167  ctex  23301  metustfbas  23601  0elsiga  23763  sigaclcu  23766  issgon  23772  insiga  23786  eupath  24309  relexpindlem  24440  dedekindle  24489  wfrlem2  24815  wfrlem3  24816  wfrlem4  24817  wfrlem9  24822  wfrlem12  24825  frrlem2  24840  frrlem3  24841  frrlem4  24842  frrlem5e  24847  frrlem11  24851  txpss3v  24976  pprodss4v  24982  elfix  25001  dffix2  25003  elsingles  25015  fnimage  25026  funpartlem  25039  funpartfun  25040  dfrdg4  25047  axcontlem4  25154  colinearex  25242  ovoliunnfl  25488  voliunnfl  25490  volsupnfl  25491  indexdom  25737  prtlem16  26060  sbccomieg  26193  setindtr  26440  setindtrs  26441  dfac11  26483  lnmlmic  26509  gicabl  26586  isnumbasgrplem1  26589  lmiclbs  26630  lmisfree  26635  iotain  26940  iotavalb  26953  sbiota1  26957  fnchoice  27023  stoweidlem53  27125  eldmrexrnb  27427  mpt2xopxnop0  27435  hash1snb  27473  hasheqf1oi  27476  brfi1uzind  27489  usgraedg4  27552  edgusgranbfin  27605  uvtx01vtx  27638  3v3e3cycl2  27771  vdfrgra0  27838  vdgfrgra0  27839  frgrawopreglem2  27861  bnj521  28510  bnj906  28707  bnj938  28714  bnj1018  28739  bnj1020  28740  bnj1125  28767  bnj1145  28768  equvinNEW7  28933
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-ex 1542
  Copyright terms: Public domain W3C validator