![]() |
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 2473 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sp 1522 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylbi 121 |
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 106 ax-4 1521 |
This theorem depends on definitions: df-bi 117 df-ral 2473 |
This theorem is referenced by: rspa 2538 rsp2 2540 rspec 2542 r19.12 2596 ralbi 2622 rexbi 2623 reupick2 3436 dfiun2g 3933 iinss2 3954 invdisj 4012 mpteq12f 4098 trss 4125 sowlin 4338 reusv1 4476 reusv3 4478 ralxfrALT 4485 funimaexglem 5318 fun11iun 5501 fvmptssdm 5620 ffnfv 5694 riota5f 5875 mpoeq123 5954 tfri3 6391 nneneq 6884 mkvprop 7185 cauappcvgprlemladdru 7684 cauappcvgprlemladdrl 7685 caucvgprlemm 7696 suplocexprlemss 7743 suplocsrlem 7836 indstr 9622 prodeq2 11596 fprodle 11679 bezoutlemzz 12034 sgrpidmndm 12878 srgdilem 13320 ringdilem 13363 tgcl 14016 fsumcncntop 14508 dedekindeulemlu 14551 dedekindicclemlu 14560 bj-rspgt 14991 bj-charfunr 15015 |
Copyright terms: Public domain | W3C validator |