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

Theorem exlimiv 1486
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 1486 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 1416 . 2
2 exlimiv.1 . 2
31, 2exlimih 1481 1
Colors of variables: wff set class
Syntax hints:   wi 4  wex 1378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1335  ax-ie2 1380  ax-17 1416
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11v  1705  ax11ev  1706  equs5or  1708  exlimivv  1773  mo23  1938  mopick  1975  gencl  2580  cgsexg  2583  gencbvex2  2595  vtocleg  2618  eqvinc  2661  eqvincg  2662  elrabi  2689  sbcex2  2806  oprcl  3564  eluni  3574  intab  3635  uniintsnr  3642  trint0m  3862  bm1.3ii  3869  inteximm  3894  axpweq  3915  bnd2  3917  unipw  3944  euabex  3952  mss  3953  exss  3954  opelopabsb  3988  eusvnf  4151  eusvnfb  4152  regexmidlem1  4218  eunex  4239  relop  4429  dmrnssfld  4538  xpmlem  4687  dmxpss  4696  dmsnopg  4735  elxp5  4752  iotauni  4822  iota1  4824  iota4  4828  funimaexglem  4925  ffoss  5101  relelfvdm  5148  nfvres  5149  fvelrnb  5164  eusvobj2  5441  acexmidlemv  5453  fnoprabg  5544  fo1stresm  5730  fo2ndresm  5731  eloprabi  5764  reldmtpos  5809  dftpos4  5819  tfrlem9  5876  tfrexlem  5889  ecdmn0m  6084  bren  6164  brdomg  6165  ener  6195  en0  6211  en1  6215  en1bg  6216  2dom  6221  fiprc  6228  enm  6230  ssfiexmid  6254  subhalfnqq  6397  nqnq0pi  6420  nqnq0  6423  prarloc  6485  nqprm  6525  ltexprlemm  6572  recexprlemell  6592  recexprlemelu  6593  recexprlemopl  6595  recexprlemopu  6597  recexprlempr  6602  fzm  8632  fzom  8750  bdbm1.3ii  9279
  Copyright terms: Public domain W3C validator