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 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.) |
Ref | Expression |
---|---|
exlimiv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
exlimiv | ⊢ (∃𝑥𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1491 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
2 | exlimiv.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | exlimih 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 |