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

Theorem exlimiv 1503
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 1503 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 1433 . 2 (𝜓 → ∀𝑥𝜓)
2 exlimiv.1 . 2 (𝜑𝜓)
31, 2exlimih 1498 1 (∃𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-gen 1352  ax-ie2 1397  ax-17 1433
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  ax11v  1722  ax11ev  1723  equs5or  1725  exlimivv  1790  mo23  1955  mopick  1992  gencl  2601  cgsexg  2604  gencbvex2  2616  vtocleg  2639  eqvinc  2687  eqvincg  2688  elrabi  2715  sbcex2  2836  oprcl  3598  eluni  3608  intab  3669  uniintsnr  3676  trintssm  3895  bm1.3ii  3903  inteximm  3928  axpweq  3949  bnd2  3951  unipw  3978  euabex  3986  mss  3987  exss  3988  opelopabsb  4022  eusvnf  4210  eusvnfb  4211  regexmidlem1  4283  eunex  4310  relop  4511  dmrnssfld  4620  xpmlem  4769  dmxpss  4778  dmsnopg  4817  elxp5  4834  iotauni  4904  iota1  4906  iota4  4910  funimaexglem  5007  ffoss  5183  relelfvdm  5230  nfvres  5231  fvelrnb  5246  eusvobj2  5523  acexmidlemv  5535  fnoprabg  5627  fo1stresm  5813  fo2ndresm  5814  eloprabi  5847  cnvoprab  5880  reldmtpos  5896  dftpos4  5906  tfrlem9  5963  tfrexlem  5976  ecdmn0m  6176  bren  6256  brdomg  6257  ener  6287  en0  6303  en1  6307  en1bg  6308  2dom  6313  fiprc  6320  enm  6322  php5dom  6353  ssfiexmid  6364  diffitest  6372  subhalfnqq  6540  nqnq0pi  6564  nqnq0  6567  prarloc  6629  nqprm  6668  ltexprlemm  6726  recexprlemell  6748  recexprlemelu  6749  recexprlemopl  6751  recexprlemopu  6753  recexprlempr  6758  fzm  8974  fzom  9092  fclim  10009  climmo  10013  bdbm1.3ii  10341
  Copyright terms: Public domain W3C validator