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

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

This inference, along with our many variants such as rexlimdv 2667, 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/~jlh/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 1667 to arrive at  ( E. x ph  ->  ps ). Finally, we separately prove  E. x ph and detach it with modus ponens ax-mp 10 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 1564 . 2  |-  ( E. x ph  ->  E. x ps )
3 19.9v 1664 . 2  |-  ( E. x ps  <->  ps )
42, 3sylib 190 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1529
This theorem is referenced by:  exlimivv  1668  ax12olem1  1869  equvin  1946  mo  2166  mopick  2206  gencl  2817  cgsexg  2820  gencbvex2  2832  vtocleg  2855  eqvinc  2896  sbcex2  3041  eluni  3831  intab  3893  uniintsn  3900  disjiun  4014  trint0  4131  bm1.3ii  4145  intex  4170  axpweq  4186  eunex  4202  unipw  4223  moabex  4231  nnullss  4234  exss  4235  mosubopt  4263  opelopabsb  4274  eusvnf  4528  eusvnfb  4529  reusv2lem3  4536  limuni3  4642  tfindsg  4650  findsg  4682  relop  4833  dmrnssfld  4937  dmsnopg  5142  elxp5  5159  unixp0  5204  ffoss  5470  dffv2  5553  exfo  5639  fnoprabg  5906  fo1stres  6104  fo2ndres  6105  eloprabi  6147  frxp  6186  reldmtpos  6203  dftpos4  6214  iotauni  6264  iota1  6266  iota4  6270  eusvobj2  6332  tfrlem9  6396  ecdmn0  6697  mapprc  6771  ixpprc  6832  ixpn0  6843  bren  6866  brdomg  6867  ener  6903  en0  6919  en1  6923  en1b  6924  2dom  6928  fiprc  6937  pwdom  7008  domssex  7017  ssenen  7030  php  7040  isinf  7071  findcard2s  7094  hartogslem1  7252  brwdom  7276  brwdomn0  7278  wdompwdom  7287  unxpwdom2  7297  ixpiunwdom  7300  inf3  7331  infeq5  7333  omex  7339  epfrs  7408  rankwflemb  7460  bnd2  7558  oncard  7588  carduni  7609  pm54.43  7628  ween  7657  acnrcl  7664  acndom  7673  acndom2  7676  iunfictbso  7736  aceq3lem  7742  dfac4  7744  dfac5lem4  7748  dfac5lem5  7749  dfac5  7750  dfac2a  7751  dfac2  7752  dfacacn  7762  dfac12r  7767  kmlem2  7772  kmlem16  7786  ackbij2  7864  cff  7869  cardcf  7873  cfeq0  7877  cfsuc  7878  cff1  7879  cfcoflem  7893  coftr  7894  infpssr  7929  fin4en1  7930  isfin4-2  7935  enfin2i  7942  fin23lem21  7960  fin23lem30  7963  fin23lem41  7973  enfin1ai  8005  fin1a2lem7  8027  axcc2lem  8057  domtriomlem  8063  dcomex  8068  axdc2lem  8069  axdc3lem2  8072  axdc4lem  8076  axcclem  8078  ac6s  8106  zorn2lem7  8124  ttukey2g  8138  axdclem2  8142  axdc  8143  brdom3  8148  brdom5  8149  brdom4  8150  brdom7disj  8151  brdom6disj  8152  konigthlem  8185  pwcfsdom  8200  pwfseq  8281  tsk0  8380  gruina  8435  grothpw  8443  grothpwex  8444  grothomex  8446  grothac  8447  ltbtwnnq  8597  reclem2pr  8667  supsrlem  8728  supsr  8729  axpre-sup  8786  nnunb  9956  ioorebas  10739  fzn0  10803  fzon0  10885  axdc4uzlem  11038  hashf1lem2  11388  swrdcl  11446  fclim  12021  climmo  12025  rlimdmo1  12085  cnso  12519  xpsfrnel2  13461  brssc  13685  sscpwex  13686  grpidval  14378  subgint  14635  giclcl  14730  gicrcl  14731  gicsym  14732  gicen  14735  gicsubgen  14736  cntzssv  14798  giccyg  15180  subrgint  15561  lmiclcl  15817  lmicrcl  15818  lmicsym  15819  abvn0b  16037  cmpsub  17121  iuncon  17148  2ndcsb  17169  elpt  17261  ptclsg  17303  hmphsym  17467  hmphen  17470  haushmphlem  17472  cmphmph  17473  conhmph  17474  reghmph  17478  nrmhmph  17479  hmphdis  17481  indishmph  17483  hmphen2  17484  ufldom  17651  alexsubALTlem2  17736  alexsubALT  17739  iunmbl2  18908  ioorcl2  18921  ioorinv2  18924  opnmblALT  18952  mpfrcl  19396  pf1rcl  19426  plyssc  19576  aannenlem2  19703  aannenlem3  19704  mulog2sum  20680  shintcli  21900  strlem1  22822  eupath  23309  relexpindlem  23440  dedekindle  23486  wfrlem2  23658  wfrlem3  23659  wfrlem4  23660  wfrlem9  23665  wfrlem12  23668  frrlem2  23683  frrlem3  23684  frrlem4  23685  frrlem5e  23690  frrlem11  23694  txpss3v  23826  pprodss4v  23832  elfix  23851  dffix2  23853  elsingles  23864  fnimage  23875  funpartfun  23888  dfrdg4  23895  axcontlem4  24002  colinearex  24090  copsexgb  24364  prj1b  24477  prj3  24478  prl  24566  inposet  24677  osneisi  24930  dmhmph  24932  rnhmph  24933  fisub  24953  limptlimpr2lem1  24973  bwt2  24991  indexdom  25812  prtlem16  26136  sbccomieg  26269  setindtr  26516  setindtrs  26517  dfac11  26559  lnmlmic  26585  gicabl  26662  isnumbasgrplem1  26665  lmiclbs  26706  lmisfree  26711  iotain  27016  iotavalb  27029  sbiota1  27033  fnchoice  27099  stoweidlem53  27201  bnj521  28032  bnj906  28229  bnj938  28236  bnj1018  28261  bnj1020  28262  bnj1125  28289  bnj1145  28290
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530
  Copyright terms: Public domain W3C validator