![]() |
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 x exists satisfying a wff, i.e. ∃xφ(x) where φ(x) has x 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 x) 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 x. Then we apply exlimiv 1486 to arrive at (∃xφ → ψ). Finally, we separately prove ∃xφ 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 | ⊢ (∃xφ → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1416 | . 2 ⊢ (ψ → ∀xψ) | |
2 | exlimiv.1 | . 2 ⊢ (φ → ψ) | |
3 | 1, 2 | exlimih 1481 | 1 ⊢ (∃xφ → ψ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1378 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-gen 1335 ax-ie2 1380 ax-17 1416 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ax11v 1705 ax11ev 1706 equs5or 1708 exlimivv 1773 mo23 1938 mopick 1975 gencl 2580 cgsexg 2583 gencbvex2 2595 vtocleg 2618 eqvinc 2661 eqvincg 2662 elrabi 2689 sbcex2 2806 oprcl 3564 eluni 3574 intab 3635 uniintsnr 3642 trint0m 3862 bm1.3ii 3869 inteximm 3894 axpweq 3915 bnd2 3917 unipw 3944 euabex 3952 mss 3953 exss 3954 opelopabsb 3988 eusvnf 4151 eusvnfb 4152 regexmidlem1 4218 eunex 4239 relop 4429 dmrnssfld 4538 xpmlem 4687 dmxpss 4696 dmsnopg 4735 elxp5 4752 iotauni 4822 iota1 4824 iota4 4828 funimaexglem 4925 ffoss 5101 relelfvdm 5148 nfvres 5149 fvelrnb 5164 eusvobj2 5441 acexmidlemv 5453 fnoprabg 5544 fo1stresm 5730 fo2ndresm 5731 eloprabi 5764 reldmtpos 5809 dftpos4 5819 tfrlem9 5876 tfrexlem 5889 ecdmn0m 6084 bren 6164 brdomg 6165 ener 6195 en0 6211 en1 6215 en1bg 6216 2dom 6221 fiprc 6228 enm 6230 ssfiexmid 6254 subhalfnqq 6397 nqnq0pi 6421 nqnq0 6424 prarloc 6486 nqprm 6525 ltexprlemm 6574 recexprlemell 6594 recexprlemelu 6595 recexprlemopl 6597 recexprlemopu 6599 recexprlempr 6604 fzm 8672 fzom 8790 bdbm1.3ii 9346 |
Copyright terms: Public domain | W3C validator |