ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exlimiv Unicode version

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

This inference, along with our many variants 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 1596 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, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)

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 ax-17 1524 . 2  |-  ( ps 
->  A. x ps )
2 exlimiv.1 . 2  |-  ( ph  ->  ps )
31, 2exlimih 1591 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1447  ax-ie2 1492  ax-17 1524
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ax11v  1825  ax11ev  1826  equs5or  1828  exlimivv  1894  cbvexvw  1918  mo23  2065  mopick  2102  gencl  2767  cgsexg  2770  gencbvex2  2782  vtocleg  2806  eqvinc  2858  eqvincg  2859  elrabi  2888  sbcex2  3014  oprcl  3798  eluni  3808  intab  3869  uniintsnr  3876  trintssm  4112  bm1.3ii  4119  inteximm  4144  axpweq  4166  bnd2  4168  unipw  4211  euabex  4219  mss  4220  exss  4221  opelopabsb  4254  eusvnf  4447  eusvnfb  4448  regexmidlem1  4526  eunex  4554  relop  4770  dmrnssfld  4883  xpmlem  5041  dmxpss  5051  dmsnopg  5092  elxp5  5109  iotauni  5182  iota1  5184  iota4  5188  iotam  5200  funimaexglem  5291  ffoss  5485  relelfvdm  5539  nfvres  5540  fvelrnb  5555  eusvobj2  5851  acexmidlemv  5863  fnoprabg  5966  fo1stresm  6152  fo2ndresm  6153  eloprabi  6187  cnvoprab  6225  reldmtpos  6244  dftpos4  6254  tfrlem9  6310  tfrexlem  6325  ecdmn0m  6567  mapprc  6642  ixpprc  6709  ixpm  6720  bren  6737  brdomg  6738  ener  6769  en0  6785  en1  6789  en1bg  6790  2dom  6795  fiprc  6805  enm  6810  ssenen  6841  php5dom  6853  ssfilem  6865  diffitest  6877  inffiexmid  6896  ctm  7098  ctssdclemr  7101  ctssdc  7102  enumct  7104  ctfoex  7107  ctssexmid  7138  pm54.43  7179  subhalfnqq  7388  nqnq0pi  7412  nqnq0  7415  prarloc  7477  nqprm  7516  ltexprlemm  7574  recexprlemell  7596  recexprlemelu  7597  recexprlemopl  7599  recexprlemopu  7601  recexprlempr  7606  sup3exmid  8885  fzm  10006  fzom  10132  fclim  11269  climmo  11273  ctinfom  12395  qnnen  12398  unct  12409  omiunct  12411  opifismgmdc  12655  ismgmid  12661  ismnd  12685  dfgrp2e  12763  dfgrp3me  12829  topnex  13079  bdbm1.3ii  14125
  Copyright terms: Public domain W3C validator