![]() |
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 1534 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-rex 2376 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylibr 133 |
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-ia2 106 ax-ia3 107 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-4 1452 |
This theorem depends on definitions: df-bi 116 df-rex 2376 |
This theorem is referenced by: rsp2e 2437 ssiun2 3795 tfrlem9 6122 tfrlemibxssdm 6130 tfr1onlembxssdm 6146 tfrcllembxssdm 6159 findcard2 6685 findcard2s 6686 prarloclemup 7151 prmuloc2 7223 ltaddpr 7253 aptiprlemu 7296 cauappcvgprlemopl 7302 cauappcvgprlemopu 7304 cauappcvgprlem2 7316 caucvgprlemopl 7325 caucvgprlemopu 7327 caucvgprlem2 7336 caucvgprprlem2 7366 |
Copyright terms: Public domain | W3C validator |