![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspe | Structured version Visualization version Unicode version |
Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.) |
Ref | Expression |
---|---|
rspe |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 1955 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-rex 2762 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylibr 217 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-12 1950 |
This theorem depends on definitions: df-bi 190 df-ex 1672 df-rex 2762 |
This theorem is referenced by: rsp2e 2845 2rmorex 3232 ssiun2 4312 reusv2lem3 4604 tfrlem9 7121 isinf 7803 findcard2 7829 findcard3 7832 scott0 8375 ac6c4 8929 supaddc 10596 supadd 10597 supmul1 10598 supmul 10601 mreiincl 15580 restmetu 21663 bposlem3 24293 opphllem5 24872 pjpjpre 27153 atom1d 28087 bnj1398 29915 cvmlift2lem12 30109 finminlem 31045 neibastop2lem 31087 iooelexlt 31835 relowlpssretop 31837 prtlem18 32513 pell14qrdich 35786 disjinfi 37539 iunmapsn 37570 upbdrech 37611 limclner 37829 sge0iunmptlemre 38371 iundjiun 38414 isomenndlem 38470 ovnsubaddlem1 38510 2reurex 38747 |
Copyright terms: Public domain | W3C validator |