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

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

This inference, along with our many variants such as rexlimdv 2641, 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 2024 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 nfv 1629 . 2  |-  F/ x ps
2 exlimiv.1 . 2  |-  ( ph  ->  ps )
31, 2exlimi 1781 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537
This theorem is referenced by:  exlimivv  2026  mo  2140  mopick  2180  gencl  2791  cgsexg  2794  gencbvex2  2806  vtocleg  2829  eqvinc  2870  sbcex2  3015  eluni  3804  intab  3866  uniintsn  3873  disjiun  3987  trint0  4104  bm1.3ii  4118  intex  4143  axpweq  4159  eunex  4175  unipw  4196  moabex  4204  nnullss  4207  exss  4208  mosubopt  4236  opelopabsb  4247  eusvnf  4501  eusvnfb  4502  reusv2lem3  4509  limuni3  4615  tfindsg  4623  findsg  4655  relop  4822  dmrnssfld  4926  dmsnopg  5131  elxp5  5148  unixp0  5193  ffoss  5443  dffv2  5526  exfo  5612  fnoprabg  5879  fo1stres  6077  fo2ndres  6078  eloprabi  6120  frxp  6159  reldmtpos  6176  dftpos4  6187  iotauni  6237  iota1  6239  iota4  6243  eusvobj2  6305  tfrlem9  6369  ecdmn0  6670  mapprc  6744  ixpprc  6805  ixpn0  6816  bren  6839  brdomg  6840  ener  6876  en0  6892  en1  6896  en1b  6897  2dom  6901  fiprc  6910  pwdom  6981  domssex  6990  ssenen  7003  php  7013  isinf  7044  findcard2s  7067  hartogslem1  7225  brwdom  7249  brwdomn0  7251  wdompwdom  7260  unxpwdom2  7270  ixpiunwdom  7273  inf3  7304  infeq5  7306  omex  7312  epfrs  7381  rankwflemb  7433  bnd2  7531  oncard  7561  carduni  7582  pm54.43  7601  ween  7630  acnrcl  7637  acndom  7646  acndom2  7649  iunfictbso  7709  aceq3lem  7715  dfac4  7717  dfac5lem4  7721  dfac5lem5  7722  dfac5  7723  dfac2a  7724  dfac2  7725  dfacacn  7735  dfac12r  7740  kmlem2  7745  kmlem16  7759  ackbij2  7837  cff  7842  cardcf  7846  cfeq0  7850  cfsuc  7851  cff1  7852  cfcoflem  7866  coftr  7867  infpssr  7902  fin4en1  7903  isfin4-2  7908  enfin2i  7915  fin23lem21  7933  fin23lem30  7936  fin23lem41  7946  enfin1ai  7978  fin1a2lem7  8000  axcc2lem  8030  domtriomlem  8036  dcomex  8041  axdc2lem  8042  axdc3lem2  8045  axdc4lem  8049  axcclem  8051  ac6s  8079  zorn2lem7  8097  ttukey2g  8111  axdclem2  8115  axdc  8116  brdom3  8121  brdom5  8122  brdom4  8123  brdom7disj  8124  brdom6disj  8125  konigthlem  8158  pwcfsdom  8173  pwfseq  8254  tsk0  8353  gruina  8408  grothpw  8416  grothpwex  8417  grothomex  8419  grothac  8420  ltbtwnnq  8570  reclem2pr  8640  supsrlem  8701  supsr  8702  axpre-sup  8759  nnunb  9928  ioorebas  10711  fzn0  10775  fzon0  10857  axdc4uzlem  11010  hashf1lem2  11359  swrdcl  11417  fclim  11992  climmo  11996  rlimdmo1  12056  cnso  12487  xpsfrnel2  13429  brssc  13653  sscpwex  13654  grpidval  14346  subgint  14603  giclcl  14698  gicrcl  14699  gicsym  14700  gicen  14703  gicsubgen  14704  cntzssv  14766  giccyg  15148  subrgint  15529  lmiclcl  15785  lmicrcl  15786  lmicsym  15787  abvn0b  16005  cmpsub  17089  iuncon  17116  2ndcsb  17137  elpt  17229  ptclsg  17271  hmphsym  17435  hmphen  17438  haushmphlem  17440  cmphmph  17441  conhmph  17442  reghmph  17446  nrmhmph  17447  hmphdis  17449  indishmph  17451  hmphen2  17452  ufldom  17619  alexsubALTlem2  17704  alexsubALT  17707  iunmbl2  18876  ioorcl2  18889  ioorinv2  18892  opnmblALT  18920  mpfrcl  19364  pf1rcl  19394  plyssc  19544  aannenlem2  19671  aannenlem3  19672  mulog2sum  20648  shintcli  21868  strlem1  22790  eupath  23277  relexpindlem  23408  dedekindle  23454  wfrlem2  23626  wfrlem3  23627  wfrlem4  23628  wfrlem9  23633  wfrlem12  23636  frrlem2  23651  frrlem3  23652  frrlem4  23653  frrlem5e  23658  frrlem11  23662  txpss3v  23794  pprodss4v  23800  elfix  23819  dffix2  23821  elsingles  23832  fnimage  23843  funpartfun  23856  dfrdg4  23863  axcontlem4  23970  colinearex  24058  copsexgb  24332  prj1b  24445  prj3  24446  prl  24534  inposet  24645  osneisi  24898  dmhmph  24900  rnhmph  24901  fisub  24921  limptlimpr2lem1  24941  bwt2  24959  indexdom  25780  prtlem16  26104  sbccomieg  26237  setindtr  26484  setindtrs  26485  dfac11  26527  lnmlmic  26553  gicabl  26630  isnumbasgrplem1  26633  lmiclbs  26674  lmisfree  26679  iotain  26985  iotavalb  26998  sbiota1  27002  fnchoice  27068  stoweidlem53  27137  bnj521  27814  bnj906  28011  bnj938  28018  bnj1018  28043  bnj1020  28044  bnj1125  28071  bnj1145  28072
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator