![]() |
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 2380 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sp 1456 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylbi 120 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-4 1455 |
This theorem depends on definitions: df-bi 116 df-ral 2380 |
This theorem is referenced by: rsp2 2441 rspec 2443 r19.12 2497 ralbi 2523 rexbi 2524 reupick2 3309 dfiun2g 3792 iinss2 3812 invdisj 3869 mpteq12f 3948 trss 3975 sowlin 4180 reusv1 4317 reusv3 4319 ralxfrALT 4326 funimaexglem 5142 fun11iun 5322 fvmptssdm 5437 ffnfv 5510 riota5f 5686 mpoeq123 5762 tfri3 6194 nneneq 6680 mkvprop 6943 cauappcvgprlemladdru 7365 cauappcvgprlemladdrl 7366 caucvgprlemm 7377 indstr 9238 bezoutlemzz 11483 tgcl 12015 bj-rspgt 12574 |
Copyright terms: Public domain | W3C validator |