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 1489 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 1419 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
2 | exlimiv.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | exlimih 1484 | 1 ⊢ (∃𝑥𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-gen 1338 ax-ie2 1383 ax-17 1419 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ax11v 1708 ax11ev 1709 equs5or 1711 exlimivv 1776 mo23 1941 mopick 1978 gencl 2586 cgsexg 2589 gencbvex2 2601 vtocleg 2624 eqvinc 2667 eqvincg 2668 elrabi 2695 sbcex2 2812 oprcl 3573 eluni 3583 intab 3644 uniintsnr 3651 trint0m 3871 bm1.3ii 3878 inteximm 3903 axpweq 3924 bnd2 3926 unipw 3953 euabex 3961 mss 3962 exss 3963 opelopabsb 3997 eusvnf 4185 eusvnfb 4186 regexmidlem1 4258 eunex 4285 relop 4486 dmrnssfld 4595 xpmlem 4744 dmxpss 4753 dmsnopg 4792 elxp5 4809 iotauni 4879 iota1 4881 iota4 4885 funimaexglem 4982 ffoss 5158 relelfvdm 5205 nfvres 5206 fvelrnb 5221 eusvobj2 5498 acexmidlemv 5510 fnoprabg 5602 fo1stresm 5788 fo2ndresm 5789 eloprabi 5822 reldmtpos 5868 dftpos4 5878 tfrlem9 5935 tfrexlem 5948 ecdmn0m 6148 bren 6228 brdomg 6229 ener 6259 en0 6275 en1 6279 en1bg 6280 2dom 6285 fiprc 6292 enm 6294 php5dom 6325 ssfiexmid 6336 diffitest 6344 subhalfnqq 6512 nqnq0pi 6536 nqnq0 6539 prarloc 6601 nqprm 6640 ltexprlemm 6698 recexprlemell 6720 recexprlemelu 6721 recexprlemopl 6723 recexprlemopu 6725 recexprlempr 6730 fzm 8902 fzom 9020 fclim 9815 climmo 9819 bdbm1.3ii 10011 |
Copyright terms: Public domain | W3C validator |