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

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

This inference, along with our many variants such as rexlimdv 2666, 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 1666 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.)

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 1563 . 2  |-  ( E. x ph  ->  E. x ps )
3 19.9v 1663 . 2  |-  ( E. x ps  <->  ps )
42, 3sylib 188 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  exlimivv  1667  ax12olem1  1868  equvin  1941  mo  2165  mopick  2205  gencl  2816  cgsexg  2819  gencbvex2  2831  vtocleg  2854  eqvinc  2895  sbcex2  3040  eluni  3830  intab  3892  uniintsn  3899  disjiun  4013  trint0  4130  bm1.3ii  4144  intex  4167  axpweq  4187  eunex  4203  unipw  4224  moabex  4232  nnullss  4235  exss  4236  mosubopt  4264  opelopabsb  4275  eusvnf  4529  eusvnfb  4530  reusv2lem3  4537  limuni3  4643  tfindsg  4651  findsg  4683  relop  4834  dmrnssfld  4938  dmsnopg  5144  elxp5  5161  unixp0  5206  iotauni  5231  iota1  5233  iota4  5237  ffoss  5505  dffv2  5592  exfo  5678  fnoprabg  5945  fo1stres  6143  fo2ndres  6144  eloprabi  6186  frxp  6225  reldmtpos  6242  dftpos4  6253  eusvobj2  6337  tfrlem9  6401  ecdmn0  6702  mapprc  6776  ixpprc  6837  ixpn0  6848  bren  6871  brdomg  6872  ener  6908  en0  6924  en1  6928  en1b  6929  2dom  6933  fiprc  6942  pwdom  7013  domssex  7022  ssenen  7035  php  7045  isinf  7076  findcard2s  7099  hartogslem1  7257  brwdom  7281  brwdomn0  7283  wdompwdom  7292  unxpwdom2  7302  ixpiunwdom  7305  inf3  7336  infeq5  7338  omex  7344  epfrs  7413  rankwflemb  7465  bnd2  7563  oncard  7593  carduni  7614  pm54.43  7633  ween  7662  acnrcl  7669  acndom  7678  acndom2  7681  iunfictbso  7741  aceq3lem  7747  dfac4  7749  dfac5lem4  7753  dfac5lem5  7754  dfac5  7755  dfac2a  7756  dfac2  7757  dfacacn  7767  dfac12r  7772  kmlem2  7777  kmlem16  7791  ackbij2  7869  cff  7874  cardcf  7878  cfeq0  7882  cfsuc  7883  cff1  7884  cfcoflem  7898  coftr  7899  infpssr  7934  fin4en1  7935  isfin4-2  7940  enfin2i  7947  fin23lem21  7965  fin23lem30  7968  fin23lem41  7978  enfin1ai  8010  fin1a2lem7  8032  axcc2lem  8062  domtriomlem  8068  dcomex  8073  axdc2lem  8074  axdc3lem2  8077  axdc4lem  8081  axcclem  8083  ac6s  8111  zorn2lem7  8129  ttukey2g  8143  axdclem2  8147  axdc  8148  brdom3  8153  brdom5  8154  brdom4  8155  brdom7disj  8156  brdom6disj  8157  konigthlem  8190  pwcfsdom  8205  pwfseq  8286  tsk0  8385  gruina  8440  grothpw  8448  grothpwex  8449  grothomex  8451  grothac  8452  ltbtwnnq  8602  reclem2pr  8672  supsrlem  8733  supsr  8734  axpre-sup  8791  nnunb  9961  ioorebas  10745  fzn0  10809  fzon0  10891  axdc4uzlem  11044  hashf1lem2  11394  swrdcl  11452  fclim  12027  climmo  12031  rlimdmo1  12091  cnso  12525  xpsfrnel2  13467  brssc  13691  sscpwex  13692  grpidval  14384  subgint  14641  giclcl  14736  gicrcl  14737  gicsym  14738  gicen  14741  gicsubgen  14742  cntzssv  14804  giccyg  15186  subrgint  15567  lmiclcl  15823  lmicrcl  15824  lmicsym  15825  abvn0b  16043  cmpsub  17127  iuncon  17154  2ndcsb  17175  elpt  17267  ptclsg  17309  hmphsym  17473  hmphen  17476  haushmphlem  17478  cmphmph  17479  conhmph  17480  reghmph  17484  nrmhmph  17485  hmphdis  17487  indishmph  17489  hmphen2  17490  ufldom  17657  alexsubALTlem2  17742  alexsubALT  17745  iunmbl2  18914  ioorcl2  18927  ioorinv2  18930  opnmblALT  18958  mpfrcl  19402  pf1rcl  19432  plyssc  19582  aannenlem2  19709  aannenlem3  19710  mulog2sum  20686  shintcli  21908  strlem1  22830  eupath  23316  relexpindlem  23447  dedekindle  23494  wfrlem2  23668  wfrlem3  23669  wfrlem4  23670  wfrlem9  23675  wfrlem12  23678  frrlem2  23693  frrlem3  23694  frrlem4  23695  frrlem5e  23700  frrlem11  23704  txpss3v  23829  pprodss4v  23835  elfix  23854  dffix2  23856  elsingles  23868  fnimage  23879  funpartfun  23892  dfrdg4  23899  axcontlem4  24006  colinearex  24094  copsexgb  24378  prj1b  24491  prj3  24492  prl  24579  inposet  24690  osneisi  24943  dmhmph  24945  rnhmph  24946  fisub  24966  limptlimpr2lem1  24986  bwt2  25004  indexdom  25825  prtlem16  26149  sbccomieg  26282  setindtr  26529  setindtrs  26530  dfac11  26572  lnmlmic  26598  gicabl  26675  isnumbasgrplem1  26678  lmiclbs  26719  lmisfree  26724  iotain  27029  iotavalb  27042  sbiota1  27046  fnchoice  27112  stoweidlem53  27214  bnj521  28138  bnj906  28335  bnj938  28342  bnj1018  28367  bnj1020  28368  bnj1125  28395  bnj1145  28396
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator