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

Theorem exlimiv 1577
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 1577 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 1506 . 2  |-  ( ps 
->  A. x ps )
2 exlimiv.1 . 2  |-  ( ph  ->  ps )
31, 2exlimih 1572 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1425  ax-ie2 1470  ax-17 1506
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11v  1799  ax11ev  1800  equs5or  1802  exlimivv  1868  mo23  2040  mopick  2077  gencl  2718  cgsexg  2721  gencbvex2  2733  vtocleg  2757  eqvinc  2808  eqvincg  2809  elrabi  2837  sbcex2  2962  oprcl  3729  eluni  3739  intab  3800  uniintsnr  3807  trintssm  4042  bm1.3ii  4049  inteximm  4074  axpweq  4095  bnd2  4097  unipw  4139  euabex  4147  mss  4148  exss  4149  opelopabsb  4182  eusvnf  4374  eusvnfb  4375  regexmidlem1  4448  eunex  4476  relop  4689  dmrnssfld  4802  xpmlem  4959  dmxpss  4969  dmsnopg  5010  elxp5  5027  iotauni  5100  iota1  5102  iota4  5106  funimaexglem  5206  ffoss  5399  relelfvdm  5453  nfvres  5454  fvelrnb  5469  eusvobj2  5760  acexmidlemv  5772  fnoprabg  5872  fo1stresm  6059  fo2ndresm  6060  eloprabi  6094  cnvoprab  6131  reldmtpos  6150  dftpos4  6160  tfrlem9  6216  tfrexlem  6231  ecdmn0m  6471  mapprc  6546  ixpprc  6613  ixpm  6624  bren  6641  brdomg  6642  ener  6673  en0  6689  en1  6693  en1bg  6694  2dom  6699  fiprc  6709  enm  6714  ssenen  6745  php5dom  6757  ssfilem  6769  diffitest  6781  inffiexmid  6800  ctm  6994  ctssdclemr  6997  ctssdc  6998  enumct  7000  ctfoex  7003  ctssexmid  7024  pm54.43  7046  subhalfnqq  7229  nqnq0pi  7253  nqnq0  7256  prarloc  7318  nqprm  7357  ltexprlemm  7415  recexprlemell  7437  recexprlemelu  7438  recexprlemopl  7440  recexprlemopu  7442  recexprlempr  7447  sup3exmid  8722  fzm  9825  fzom  9948  fclim  11070  climmo  11074  ctinfom  11948  qnnen  11951  unct  11962  omiunct  11964  topnex  12265  bdbm1.3ii  13119
  Copyright terms: Public domain W3C validator