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

Theorem exlimiv 1562
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 1562 to arrive at (∃𝑥𝜑𝜓). Finally, we separately prove 𝑥𝜑 and detach it with modus ponens ax-mp 5 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 1491 . 2 (𝜓 → ∀𝑥𝜓)
2 exlimiv.1 . 2 (𝜑𝜓)
31, 2exlimih 1557 1 (∃𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1410  ax-ie2 1455  ax-17 1491
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11v  1783  ax11ev  1784  equs5or  1786  exlimivv  1852  mo23  2018  mopick  2055  gencl  2692  cgsexg  2695  gencbvex2  2707  vtocleg  2731  eqvinc  2782  eqvincg  2783  elrabi  2810  sbcex2  2934  oprcl  3699  eluni  3709  intab  3770  uniintsnr  3777  trintssm  4012  bm1.3ii  4019  inteximm  4044  axpweq  4065  bnd2  4067  unipw  4109  euabex  4117  mss  4118  exss  4119  opelopabsb  4152  eusvnf  4344  eusvnfb  4345  regexmidlem1  4418  eunex  4446  relop  4659  dmrnssfld  4772  xpmlem  4929  dmxpss  4939  dmsnopg  4980  elxp5  4997  iotauni  5070  iota1  5072  iota4  5076  funimaexglem  5176  ffoss  5367  relelfvdm  5421  nfvres  5422  fvelrnb  5437  eusvobj2  5728  acexmidlemv  5740  fnoprabg  5840  fo1stresm  6027  fo2ndresm  6028  eloprabi  6062  cnvoprab  6099  reldmtpos  6118  dftpos4  6128  tfrlem9  6184  tfrexlem  6199  ecdmn0m  6439  mapprc  6514  ixpprc  6581  ixpm  6592  bren  6609  brdomg  6610  ener  6641  en0  6657  en1  6661  en1bg  6662  2dom  6667  fiprc  6677  enm  6682  ssenen  6713  php5dom  6725  ssfilem  6737  diffitest  6749  inffiexmid  6768  ctm  6962  ctssdclemr  6965  ctssdc  6966  enumct  6968  ctfoex  6971  ctssexmid  6992  pm54.43  7014  subhalfnqq  7190  nqnq0pi  7214  nqnq0  7217  prarloc  7279  nqprm  7318  ltexprlemm  7376  recexprlemell  7398  recexprlemelu  7399  recexprlemopl  7401  recexprlemopu  7403  recexprlempr  7408  sup3exmid  8683  fzm  9786  fzom  9909  fclim  11031  climmo  11035  ctinfom  11868  qnnen  11871  unct  11881  topnex  12182  bdbm1.3ii  13016
  Copyright terms: Public domain W3C validator