![]() |
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 1598 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 1526 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
2 | exlimiv.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | exlimih 1593 | 1 ⊢ (∃𝑥𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-gen 1449 ax-ie2 1494 ax-17 1526 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ax11v 1827 ax11ev 1828 equs5or 1830 exlimivv 1896 cbvexvw 1920 mo23 2067 mopick 2104 gencl 2771 cgsexg 2774 gencbvex2 2786 vtocleg 2810 eqvinc 2862 eqvincg 2863 elrabi 2892 sbcex2 3018 oprcl 3804 eluni 3814 intab 3875 uniintsnr 3882 trintssm 4119 bm1.3ii 4126 inteximm 4151 axpweq 4173 bnd2 4175 unipw 4219 euabex 4227 mss 4228 exss 4229 opelopabsb 4262 eusvnf 4455 eusvnfb 4456 regexmidlem1 4534 eunex 4562 relop 4779 dmrnssfld 4892 xpmlem 5051 dmxpss 5061 dmsnopg 5102 elxp5 5119 iotauni 5192 iota1 5194 iota4 5198 iotam 5210 funimaexglem 5301 ffoss 5495 relelfvdm 5549 nfvres 5550 fvelrnb 5566 eusvobj2 5864 acexmidlemv 5876 fnoprabg 5979 fo1stresm 6165 fo2ndresm 6166 eloprabi 6200 cnvoprab 6238 reldmtpos 6257 dftpos4 6267 tfrlem9 6323 tfrexlem 6338 ecdmn0m 6580 mapprc 6655 ixpprc 6722 ixpm 6733 bren 6750 brdomg 6751 ener 6782 en0 6798 en1 6802 en1bg 6803 2dom 6808 fiprc 6818 enm 6823 ssenen 6854 php5dom 6866 ssfilem 6878 diffitest 6890 inffiexmid 6909 ctm 7111 ctssdclemr 7114 ctssdc 7115 enumct 7117 ctfoex 7120 ctssexmid 7151 pm54.43 7192 subhalfnqq 7416 nqnq0pi 7440 nqnq0 7443 prarloc 7505 nqprm 7544 ltexprlemm 7602 recexprlemell 7624 recexprlemelu 7625 recexprlemopl 7627 recexprlemopu 7629 recexprlempr 7634 sup3exmid 8917 fzm 10041 fzom 10167 fclim 11305 climmo 11309 ctinfom 12432 qnnen 12435 unct 12446 omiunct 12448 opifismgmdc 12796 ismgmid 12802 ismnd 12826 dfgrp2e 12909 dfgrp3me 12976 subgintm 13064 topnex 13726 bdbm1.3ii 14783 |
Copyright terms: Public domain | W3C validator |