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

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

This inference, along with our many variants such as rexlimdv 2953, 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  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 (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  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 1698 to arrive at  ( E. x ph  ->  ps ). Finally, we separately prove  E. x ph and detach it with modus ponens ax-mp 5 to arrive at the final theorem  ps. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1719 and ax-8 1769. (Revised by Wolf Lammen, 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 1635 . 2  |-  ( E. x ph  ->  E. x ps )
3 ax5e 1682 . 2  |-  ( E. x ps  ->  ps )
42, 3syl 16 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  exlimivv  1699  equvin  1753  ax12v  1804  ax12vOLD  1805  19.8a  1806  19.8aOLD  1807  ax6e  1971  axc11n  2022  axc11nOLD  2023  equvinOLD  2063  sbcom2  2173  euex  2303  mo3  2320  mo3OLD  2321  moOLD  2327  mopick  2361  mopickOLD  2362  mopickOLDOLD  2363  axext3  2447  gencl  3143  cgsexg  3146  gencbvex2  3158  vtocleg  3184  eqvinc  3230  elrabi  3258  sbcex2  3385  eluni  4248  intab  4312  uniintsn  4319  disjiun  4437  trint0  4557  bm1.3ii  4571  intex  4603  axpweq  4624  eunex  4640  eusvnf  4642  eusvnfb  4643  reusv2lem3  4650  unipw  4697  moabex  4706  nnullss  4709  exss  4710  mosubopt  4745  opelopabsb  4757  relop  5151  dmrnssfld  5259  dmsnopg  5477  unixp0  5539  iotauni  5561  iota1  5563  iota4  5567  dffv2  5938  eldmrexrnb  6026  exfo  6037  csbriota  6255  eusvobj2  6275  fnoprabg  6385  limuni3  6665  tfindsg  6673  findsg  6705  elxp5  6726  f1oexbi  6731  ffoss  6742  fo1stres  6805  fo2ndres  6806  eloprabi  6843  frxp  6890  suppimacnv  6909  mpt2xopxnop0  6940  reldmtpos  6960  dftpos4  6971  tfrlem9  7051  ecdmn0  7351  mapprc  7421  ixpprc  7487  ixpn0  7498  bren  7522  brdomg  7523  ener  7559  en0  7575  en1  7579  en1b  7580  2dom  7585  fiprc  7594  pwdom  7666  domssex  7675  ssenen  7688  php  7698  isinf  7730  findcard2s  7757  hartogslem1  7963  brwdom  7989  brwdomn0  7991  wdompwdom  8000  unxpwdom2  8010  ixpiunwdom  8013  inf3  8048  infeq5  8050  omex  8056  epfrs  8158  rankwflemb  8207  bnd2  8307  oncard  8337  carduni  8358  pm54.43  8377  ween  8412  acnrcl  8419  acndom  8428  acndom2  8431  iunfictbso  8491  aceq3lem  8497  dfac4  8499  dfac5lem4  8503  dfac5lem5  8504  dfac5  8505  dfac2a  8506  dfac2  8507  dfacacn  8517  dfac12r  8522  kmlem2  8527  kmlem16  8541  ackbij2  8619  cff  8624  cardcf  8628  cfeq0  8632  cfsuc  8633  cff1  8634  cfcoflem  8648  coftr  8649  infpssr  8684  fin4en1  8685  isfin4-2  8690  enfin2i  8697  fin23lem21  8715  fin23lem30  8718  fin23lem41  8728  enfin1ai  8760  fin1a2lem7  8782  axcc2lem  8812  domtriomlem  8818  dcomex  8823  axdc2lem  8824  axdc3lem2  8827  axdc4lem  8831  axcclem  8833  ac6s  8860  zorn2lem7  8878  ttukey2g  8892  axdclem2  8896  axdc  8897  brdom3  8902  brdom5  8903  brdom4  8904  brdom7disj  8905  brdom6disj  8906  konigthlem  8939  pwcfsdom  8954  pwfseq  9038  tsk0  9137  gruina  9192  grothpw  9200  grothpwex  9201  grothomex  9203  grothac  9204  ltbtwnnq  9352  reclem2pr  9422  supsrlem  9484  supsr  9485  axpre-sup  9542  dedekindle  9740  nnunb  10787  ioorebas  11622  fzn0  11696  fzon0  11809  axdc4uzlem  12056  hasheqf1oi  12388  hash1snb  12440  hashf1lem2  12467  hashge3el3dif  12486  brfi1uzind  12494  swrdcl  12605  fclim  13335  climmo  13339  rlimdmo1  13399  cnso  13837  xpsfrnel2  14816  brssc  15040  sscpwex  15041  grpidval  15745  subgint  16020  giclcl  16115  gicrcl  16116  gicsym  16117  gicen  16120  gicsubgen  16121  cntzssv  16161  giccyg  16693  brric2  17177  ricgic  17178  subrgint  17234  lmiclcl  17499  lmicrcl  17500  lmicsym  17501  abvn0b  17722  mpfrcl  17958  ply1frcl  18126  pf1rcl  18156  lmiclbs  18639  lmisfree  18644  lmictra  18647  mat1scmat  18808  neitr  19447  cmpsub  19666  bwth  19676  bwthOLD  19677  iuncon  19695  2ndcsb  19716  elpt  19808  ptclsg  19851  hmphsym  20018  hmphen  20021  haushmphlem  20023  cmphmph  20024  conhmph  20025  reghmph  20029  nrmhmph  20030  hmphdis  20032  indishmph  20034  hmphen2  20035  ufldom  20198  alexsubALTlem2  20283  alexsubALT  20286  metustfbasOLD  20803  metustfbas  20804  iunmbl2  21702  ioorcl2  21716  ioorinv2  21719  opnmblALT  21747  plyssc  22332  aannenlem2  22459  aannenlem3  22460  mulog2sum  23450  istrkg2ld  23586  tgldim0eq  23622  axcontlem4  23946  usgraedg4  24063  edgusgranbfin  24126  uvtx01vtx  24168  3v3e3cycl2  24340  wlknwwlknsur  24388  wlkiswwlksur  24395  wwlknndef  24413  wlk0  24437  clwwlknndef  24449  2spontn0vne  24563  rusgrasn  24621  eupath  24657  vdfrgra0  24698  vdgfrgra0  24699  usgn0fidegnn0  24706  frgrawopreglem2  24722  friendship  24799  shintcli  25923  strlem1  26845  eqvincg  27050  rexunirn  27066  ctex  27203  cnvoprab  27218  prsdm  27532  prsrn  27533  0elsiga  27754  sigaclcu  27757  issgon  27763  insiga  27777  relexpindlem  28537  wfrlem2  28921  wfrlem3  28922  wfrlem4  28923  wfrlem9  28928  wfrlem12  28931  frrlem2  28965  frrlem3  28966  frrlem4  28967  frrlem5e  28972  frrlem11  28976  txpss3v  29105  pprodss4v  29111  elsingles  29145  fnimage  29156  funpartlem  29169  funpartfun  29170  dfrdg4  29177  colinearex  29287  wl-sbcom2d  29588  wl-mo3t  29598  mblfinlem3  29630  ovoliunnfl  29633  voliunnfl  29635  volsupnfl  29636  indexdom  29828  prtlem16  30214  sbccomieg  30330  setindtr  30570  setindtrs  30571  dfac11  30612  lnmlmic  30638  gicabl  30651  isnumbasgrplem1  30654  iotain  30902  iotavalb  30915  sbiota1  30919  fnchoice  30982  stoweidlem59  31359  iopmapxp  31960  iunconlem2  32815  bnj521  32872  bnj906  33067  bnj938  33074  bnj1018  33099  bnj1020  33100  bnj1125  33127  bnj1145  33128  bj-axc11nv  33397  bj-eunex  33466  bj-snglex  33612  frege55b  36889  frege55c  36910
  Copyright terms: Public domain W3C validator