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

Theorem exlimiv 1462
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 exists satisfying a wff, i.e. where has free, then we can use 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 (containing ) as an antecedent for the main part of the proof. We eventually arrive at where is the theorem to be proved and does not contain . Then we apply exlimiv 1462 to arrive at . Finally, we separately prove and detach it with modus ponens ax-mp 7 to arrive at the final theorem . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)

Hypothesis
Ref Expression
exlimiv.1
Assertion
Ref Expression
exlimiv
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem exlimiv
StepHypRef Expression
1 ax-17 1392 . 2
2 exlimiv.1 . 2
31, 2exlimih 1457 1
Colors of variables: wff set class
Syntax hints:   wi 4  wex 1354
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1311  ax-ie2 1356  ax-17 1392
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11v  1681  ax11ev  1682  equs5or  1684  exlimivv  1749  mo23  1914  mopick  1951  gencl  2554  cgsexg  2557  gencbvex2  2569  vtocleg  2592  eqvinc  2635  eqvincg  2636  elrabi  2663  sbcex2  2780  oprcl  3536  eluni  3546  intab  3607  uniintsnr  3614  trint0m  3834  bm1.3ii  3841  inteximm  3866  axpweq  3887  bnd2  3889  unipw  3916  euabex  3924  mss  3925  exss  3926  opelopabsb  3960  eusvnf  4123  eusvnfb  4124  regexmidlem1  4190  eunex  4211  relop  4401  dmrnssfld  4510  xpmlem  4659  dmxpss  4668  dmsnopg  4707  elxp5  4724  iotauni  4794  iota1  4796  iota4  4800  funimaexglem  4896  ffoss  5071  relelfvdm  5118  nfvres  5119  fvelrnb  5134  eusvobj2  5410  acexmidlemv  5422  fnoprabg  5513  fo1stresm  5699  fo2ndresm  5700  eloprabi  5733  reldmtpos  5778  dftpos4  5788  tfrlem9  5845  tfrexlem  5858  ecdmn0m  6047  subhalfnqq  6257  nqnq0pi  6279  nqnq0  6282  prarloc  6343  nqprm  6383  ltexprlemm  6423  recexprlemell  6443  recexprlemelu  6444  recexprlemopl  6446  recexprlemopu  6448  recexprlempr  6453  bdbm1.3ii  8275
  Copyright terms: Public domain W3C validator