![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > rspe | Structured version Unicode version |
Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.) |
Ref | Expression |
---|---|
rspe |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 1797 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-rex 2804 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylibr 212 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-12 1794 |
This theorem depends on definitions: df-bi 185 df-ex 1588 df-rex 2804 |
This theorem is referenced by: rsp2e 2895 2rmorex 3269 ssiun2 4320 reusv2lem3 4602 tfrlem9 6953 isinf 7636 findcard2 7662 findcard3 7665 scott0 8203 ac6c4 8760 supmul1 10405 supmul 10408 mreiincl 14652 restmetu 20293 bposlem3 22757 pjpjpre 24973 atom1d 25908 cvmlift2lem12 27346 supaddc 28564 supadd 28565 finminlem 28660 neibastop2lem 28728 prtlem18 29169 pell14qrdich 29357 2reurex 30152 bnj1398 32342 |
Copyright terms: Public domain | W3C validator |