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

Theorem exlimiv 1530
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 1530 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 1460 . 2 (𝜓 → ∀𝑥𝜓)
2 exlimiv.1 . 2 (𝜑𝜓)
31, 2exlimih 1525 1 (∃𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-17 1460
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ax11v  1749  ax11ev  1750  equs5or  1752  exlimivv  1818  mo23  1983  mopick  2020  gencl  2632  cgsexg  2635  gencbvex2  2647  vtocleg  2670  eqvinc  2719  eqvincg  2720  elrabi  2747  sbcex2  2868  oprcl  3596  eluni  3606  intab  3667  uniintsnr  3674  trintssm  3893  bm1.3ii  3901  inteximm  3926  axpweq  3947  bnd2  3949  unipw  3974  euabex  3982  mss  3983  exss  3984  opelopabsb  4017  eusvnf  4205  eusvnfb  4206  regexmidlem1  4278  eunex  4306  relop  4508  dmrnssfld  4617  xpmlem  4768  dmxpss  4777  dmsnopg  4816  elxp5  4833  iotauni  4903  iota1  4905  iota4  4909  funimaexglem  5007  ffoss  5183  relelfvdm  5231  nfvres  5232  fvelrnb  5247  eusvobj2  5523  acexmidlemv  5535  fnoprabg  5627  fo1stresm  5813  fo2ndresm  5814  eloprabi  5847  cnvoprab  5880  reldmtpos  5896  dftpos4  5906  tfrlem9  5962  tfrexlem  5977  ecdmn0m  6207  bren  6287  brdomg  6288  ener  6318  en0  6334  en1  6338  en1bg  6339  2dom  6344  fiprc  6351  enm  6354  php5dom  6388  ssfilem  6400  diffitest  6411  pm54.43  6508  subhalfnqq  6655  nqnq0pi  6679  nqnq0  6682  prarloc  6744  nqprm  6783  ltexprlemm  6841  recexprlemell  6863  recexprlemelu  6864  recexprlemopl  6866  recexprlemopu  6868  recexprlempr  6873  fzm  9122  fzom  9239  fclim  10260  climmo  10264  bdbm1.3ii  10825
  Copyright terms: Public domain W3C validator