Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rsp | Unicode version |
Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.) |
Ref | Expression |
---|---|
rsp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2447 | . 2 | |
2 | sp 1498 | . 2 | |
3 | 1, 2 | sylbi 120 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1340 wcel 2135 wral 2442 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-4 1497 |
This theorem depends on definitions: df-bi 116 df-ral 2447 |
This theorem is referenced by: rspa 2512 rsp2 2514 rspec 2516 r19.12 2570 ralbi 2596 rexbi 2597 reupick2 3403 dfiun2g 3892 iinss2 3912 invdisj 3970 mpteq12f 4056 trss 4083 sowlin 4292 reusv1 4430 reusv3 4432 ralxfrALT 4439 funimaexglem 5265 fun11iun 5447 fvmptssdm 5564 ffnfv 5637 riota5f 5816 mpoeq123 5892 tfri3 6326 nneneq 6814 mkvprop 7113 cauappcvgprlemladdru 7588 cauappcvgprlemladdrl 7589 caucvgprlemm 7600 suplocexprlemss 7647 suplocsrlem 7740 indstr 9522 prodeq2 11484 fprodle 11567 bezoutlemzz 11920 tgcl 12611 fsumcncntop 13103 dedekindeulemlu 13146 dedekindicclemlu 13155 bj-rspgt 13508 bj-charfunr 13533 |
Copyright terms: Public domain | W3C validator |