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

Theorem exlimiv 1471
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. xφ(x) where φ(x) has x 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 x) 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 x. Then we apply exlimiv 1471 to arrive at (xφψ). Finally, we separately prove xφ 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 (xφψ)
Distinct variable group:   ψ,x
Allowed substitution hint:   φ(x)

Proof of Theorem exlimiv
StepHypRef Expression
1 ax-17 1400 . 2 (ψxψ)
2 exlimiv.1 . 2 (φψ)
31, 2exlimih 1466 1 (xφψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1362
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1318  ax-ie2 1364  ax-17 1400
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11v  1690  ax11ev  1691  equs5or  1693  exlimivv  1758  mo23  1923  mopick  1960  gencl  2563  cgsexg  2566  gencbvex2  2578  vtocleg  2601  eqvinc  2644  eqvincg  2645  elrabi  2672  sbcex2  2789  oprcl  3547  eluni  3557  intab  3618  uniintsnr  3625  trint0m  3845  bm1.3ii  3852  inteximm  3877  axpweq  3898  bnd2  3900  unipw  3927  euabex  3935  mss  3936  exss  3937  opelopabsb  3971  eusvnf  4135  eusvnfb  4136  regexmidlem1  4202  eunex  4223  relop  4413  dmrnssfld  4522  xpmlem  4671  dmxpss  4680  dmsnopg  4719  elxp5  4736  iotauni  4806  iota1  4808  iota4  4812  funimaexglem  4908  ffoss  5083  relelfvdm  5130  nfvres  5131  fvelrnb  5146  eusvobj2  5422  acexmidlemv  5434  fnoprabg  5525  fo1stresm  5711  fo2ndresm  5712  eloprabi  5745  reldmtpos  5790  dftpos4  5800  tfrlem9  5857  tfrexlem  5870  ecdmn0m  6059  subhalfnqq  6271  nqnq0pi  6293  nqnq0  6296  prarloc  6357  nqprm  6397  ltexprlemm  6437  recexprlemell  6456  recexprlemelu  6457  recexprlemopl  6459  recexprlemopu  6461  recexprlempr  6466  bdbm1.3ii  7117
  Copyright terms: Public domain W3C validator