![]() |
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
We cannot do this in Metamath directly. Instead, we use the original
|
Ref | Expression |
---|---|
exlimiv.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
exlimiv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1507 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | exlimiv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | exlimih 1573 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-gen 1426 ax-ie2 1471 ax-17 1507 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v 1800 ax11ev 1801 equs5or 1803 exlimivv 1869 mo23 2041 mopick 2078 gencl 2721 cgsexg 2724 gencbvex2 2736 vtocleg 2760 eqvinc 2812 eqvincg 2813 elrabi 2841 sbcex2 2966 oprcl 3737 eluni 3747 intab 3808 uniintsnr 3815 trintssm 4050 bm1.3ii 4057 inteximm 4082 axpweq 4103 bnd2 4105 unipw 4147 euabex 4155 mss 4156 exss 4157 opelopabsb 4190 eusvnf 4382 eusvnfb 4383 regexmidlem1 4456 eunex 4484 relop 4697 dmrnssfld 4810 xpmlem 4967 dmxpss 4977 dmsnopg 5018 elxp5 5035 iotauni 5108 iota1 5110 iota4 5114 funimaexglem 5214 ffoss 5407 relelfvdm 5461 nfvres 5462 fvelrnb 5477 eusvobj2 5768 acexmidlemv 5780 fnoprabg 5880 fo1stresm 6067 fo2ndresm 6068 eloprabi 6102 cnvoprab 6139 reldmtpos 6158 dftpos4 6168 tfrlem9 6224 tfrexlem 6239 ecdmn0m 6479 mapprc 6554 ixpprc 6621 ixpm 6632 bren 6649 brdomg 6650 ener 6681 en0 6697 en1 6701 en1bg 6702 2dom 6707 fiprc 6717 enm 6722 ssenen 6753 php5dom 6765 ssfilem 6777 diffitest 6789 inffiexmid 6808 ctm 7002 ctssdclemr 7005 ctssdc 7006 enumct 7008 ctfoex 7011 ctssexmid 7032 pm54.43 7063 subhalfnqq 7246 nqnq0pi 7270 nqnq0 7273 prarloc 7335 nqprm 7374 ltexprlemm 7432 recexprlemell 7454 recexprlemelu 7455 recexprlemopl 7457 recexprlemopu 7459 recexprlempr 7464 sup3exmid 8739 fzm 9849 fzom 9972 fclim 11095 climmo 11099 ctinfom 11977 qnnen 11980 unct 11991 omiunct 11993 topnex 12294 bdbm1.3ii 13260 |
Copyright terms: Public domain | W3C validator |