Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rspe | Unicode version |
Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.) |
Ref | Expression |
---|---|
rspe |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 1482 | . 2 | |
2 | df-rex 2312 | . 2 | |
3 | 1, 2 | sylibr 137 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wex 1381 wcel 1393 wrex 2307 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 |
This theorem depends on definitions: df-bi 110 df-rex 2312 |
This theorem is referenced by: rsp2e 2372 ssiun2 3700 tfrlem9 5935 tfrlemibxssdm 5941 findcard2 6346 findcard2s 6347 prarloclemup 6593 prmuloc2 6665 ltaddpr 6695 aptiprlemu 6738 cauappcvgprlemopl 6744 cauappcvgprlemopu 6746 cauappcvgprlem2 6758 caucvgprlemopl 6767 caucvgprlemopu 6769 caucvgprlem2 6778 caucvgprprlem2 6808 |
Copyright terms: Public domain | W3C validator |