![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exlimiv | GIF version |
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 1535 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.) |
Ref | Expression |
---|---|
exlimiv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
exlimiv | ⊢ (∃𝑥𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1465 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
2 | exlimiv.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | exlimih 1530 | 1 ⊢ (∃𝑥𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1427 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-gen 1384 ax-ie2 1429 ax-17 1465 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v 1756 ax11ev 1757 equs5or 1759 exlimivv 1825 mo23 1990 mopick 2027 gencl 2654 cgsexg 2657 gencbvex2 2669 vtocleg 2693 eqvinc 2743 eqvincg 2744 elrabi 2771 sbcex2 2895 oprcl 3654 eluni 3664 intab 3725 uniintsnr 3732 trintssm 3960 bm1.3ii 3968 inteximm 3993 axpweq 4014 bnd2 4016 unipw 4055 euabex 4063 mss 4064 exss 4065 opelopabsb 4098 eusvnf 4290 eusvnfb 4291 regexmidlem1 4364 eunex 4392 relop 4601 dmrnssfld 4711 xpmlem 4867 dmxpss 4876 dmsnopg 4917 elxp5 4934 iotauni 5007 iota1 5009 iota4 5013 funimaexglem 5112 ffoss 5300 relelfvdm 5351 nfvres 5352 fvelrnb 5367 eusvobj2 5654 acexmidlemv 5666 fnoprabg 5762 fo1stresm 5948 fo2ndresm 5949 eloprabi 5982 cnvoprab 6015 reldmtpos 6034 dftpos4 6044 tfrlem9 6100 tfrexlem 6115 ecdmn0m 6350 mapprc 6425 ixpprc 6492 ixpm 6503 bren 6520 brdomg 6521 ener 6552 en0 6568 en1 6572 en1bg 6573 2dom 6578 fiprc 6588 enm 6592 ssenen 6623 php5dom 6635 ssfilem 6647 diffitest 6659 inffiexmid 6678 ctm 6847 enumct 6849 pm54.43 6881 subhalfnqq 7036 nqnq0pi 7060 nqnq0 7063 prarloc 7125 nqprm 7164 ltexprlemm 7222 recexprlemell 7244 recexprlemelu 7245 recexprlemopl 7247 recexprlemopu 7249 recexprlempr 7254 fzm 9515 fzom 9638 fclim 10745 climmo 10749 topnex 11849 bdbm1.3ii 12086 |
Copyright terms: Public domain | W3C validator |