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 2311 | . 2 | |
2 | sp 1401 | . 2 | |
3 | 1, 2 | sylbi 114 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1241 wcel 1393 wral 2306 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-4 1400 |
This theorem depends on definitions: df-bi 110 df-ral 2311 |
This theorem is referenced by: rsp2 2371 rspec 2373 r19.12 2422 ralbi 2445 rexbi 2446 reupick2 3223 dfiun2g 3689 iinss2 3709 invdisj 3759 mpteq12f 3837 trss 3863 sowlin 4057 reusv1 4190 reusv3 4192 ralxfrALT 4199 funimaexglem 4982 fun11iun 5147 fvmptssdm 5255 ffnfv 5323 riota5f 5492 mpt2eq123 5564 tfri3 5953 nneneq 6320 cauappcvgprlemladdru 6754 cauappcvgprlemladdrl 6755 caucvgprlemm 6766 indstr 8536 bj-rspgt 9925 |
Copyright terms: Public domain | W3C validator |