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

Theorem exlimiv 1530
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 1530 to arrive at  ( E. x ph  ->  ps ). Finally, we separately prove  E. x ph and detach it with modus ponens ax-mp 7 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 1460 . 2  |-  ( ps 
->  A. x ps )
2 exlimiv.1 . 2  |-  ( ph  ->  ps )
31, 2exlimih 1525 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-17 1460
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ax11v  1749  ax11ev  1750  equs5or  1752  exlimivv  1818  mo23  1983  mopick  2020  gencl  2632  cgsexg  2635  gencbvex2  2647  vtocleg  2670  eqvinc  2719  eqvincg  2720  elrabi  2747  sbcex2  2868  oprcl  3602  eluni  3612  intab  3673  uniintsnr  3680  trintssm  3899  bm1.3ii  3907  inteximm  3932  axpweq  3953  bnd2  3955  unipw  3980  euabex  3988  mss  3989  exss  3990  opelopabsb  4023  eusvnf  4211  eusvnfb  4212  regexmidlem1  4284  eunex  4312  relop  4514  dmrnssfld  4623  xpmlem  4774  dmxpss  4783  dmsnopg  4822  elxp5  4839  iotauni  4909  iota1  4911  iota4  4915  funimaexglem  5013  ffoss  5189  relelfvdm  5237  nfvres  5238  fvelrnb  5253  eusvobj2  5529  acexmidlemv  5541  fnoprabg  5633  fo1stresm  5819  fo2ndresm  5820  eloprabi  5853  cnvoprab  5886  reldmtpos  5902  dftpos4  5912  tfrlem9  5968  tfrexlem  5983  ecdmn0m  6214  bren  6294  brdomg  6295  ctex  6300  ener  6326  en0  6342  en1  6346  en1bg  6347  2dom  6352  fiprc  6360  enm  6364  php5dom  6398  ssfilem  6410  diffitest  6421  pm54.43  6518  subhalfnqq  6666  nqnq0pi  6690  nqnq0  6693  prarloc  6755  nqprm  6794  ltexprlemm  6852  recexprlemell  6874  recexprlemelu  6875  recexprlemopl  6877  recexprlemopu  6879  recexprlempr  6884  fzm  9133  fzom  9250  fclim  10271  climmo  10275  bdbm1.3ii  10840
  Copyright terms: Public domain W3C validator