Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exlimiv | Unicode 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 1596 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 1524 | . 2 | |
2 | exlimiv.1 | . 2 | |
3 | 1, 2 | exlimih 1591 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1490 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-gen 1447 ax-ie2 1492 ax-17 1524 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ax11v 1825 ax11ev 1826 equs5or 1828 exlimivv 1894 cbvexvw 1918 mo23 2065 mopick 2102 gencl 2767 cgsexg 2770 gencbvex2 2782 vtocleg 2806 eqvinc 2858 eqvincg 2859 elrabi 2888 sbcex2 3014 oprcl 3798 eluni 3808 intab 3869 uniintsnr 3876 trintssm 4112 bm1.3ii 4119 inteximm 4144 axpweq 4166 bnd2 4168 unipw 4211 euabex 4219 mss 4220 exss 4221 opelopabsb 4254 eusvnf 4447 eusvnfb 4448 regexmidlem1 4526 eunex 4554 relop 4770 dmrnssfld 4883 xpmlem 5041 dmxpss 5051 dmsnopg 5092 elxp5 5109 iotauni 5182 iota1 5184 iota4 5188 iotam 5200 funimaexglem 5291 ffoss 5485 relelfvdm 5539 nfvres 5540 fvelrnb 5555 eusvobj2 5851 acexmidlemv 5863 fnoprabg 5966 fo1stresm 6152 fo2ndresm 6153 eloprabi 6187 cnvoprab 6225 reldmtpos 6244 dftpos4 6254 tfrlem9 6310 tfrexlem 6325 ecdmn0m 6567 mapprc 6642 ixpprc 6709 ixpm 6720 bren 6737 brdomg 6738 ener 6769 en0 6785 en1 6789 en1bg 6790 2dom 6795 fiprc 6805 enm 6810 ssenen 6841 php5dom 6853 ssfilem 6865 diffitest 6877 inffiexmid 6896 ctm 7098 ctssdclemr 7101 ctssdc 7102 enumct 7104 ctfoex 7107 ctssexmid 7138 pm54.43 7179 subhalfnqq 7388 nqnq0pi 7412 nqnq0 7415 prarloc 7477 nqprm 7516 ltexprlemm 7574 recexprlemell 7596 recexprlemelu 7597 recexprlemopl 7599 recexprlemopu 7601 recexprlempr 7606 sup3exmid 8885 fzm 10006 fzom 10132 fclim 11269 climmo 11273 ctinfom 12395 qnnen 12398 unct 12409 omiunct 12411 opifismgmdc 12655 ismgmid 12661 ismnd 12685 dfgrp2e 12763 dfgrp3me 12829 topnex 13079 bdbm1.3ii 14125 |
Copyright terms: Public domain | W3C validator |