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 1569 | . 2 | |
2 | df-rex 2420 | . 2 | |
3 | 1, 2 | sylibr 133 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wex 1468 wcel 1480 wrex 2415 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 |
This theorem depends on definitions: df-bi 116 df-rex 2420 |
This theorem is referenced by: rsp2e 2481 ssiun2 3851 tfrlem9 6209 tfrlemibxssdm 6217 tfr1onlembxssdm 6233 tfrcllembxssdm 6246 findcard2 6776 findcard2s 6777 prarloclemup 7296 prmuloc2 7368 ltaddpr 7398 aptiprlemu 7441 cauappcvgprlemopl 7447 cauappcvgprlemopu 7449 cauappcvgprlem2 7461 caucvgprlemopl 7470 caucvgprlemopu 7472 caucvgprlem2 7481 caucvgprprlem2 7511 suplocexprlemrl 7518 suplocexprlemru 7520 suplocexprlemlub 7525 |
Copyright terms: Public domain | W3C validator |