![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspc | Structured version Visualization version Unicode version |
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) |
Ref | Expression |
---|---|
rspc.1 |
![]() ![]() ![]() ![]() |
rspc.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rspc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2753 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfcv 2602 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | nfv 1771 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | rspc.1 |
. . . . 5
![]() ![]() ![]() ![]() | |
5 | 3, 4 | nfim 2013 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | eleq1 2527 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | rspc.2 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | imbi12d 326 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 2, 5, 8 | spcgf 3140 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | pm2.43a 51 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 1, 10 | syl5bi 225 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ral 2753 df-v 3058 |
This theorem is referenced by: rspcv 3157 rspc2 3169 disjxiun 4412 pofun 4789 fmptcof 6080 fliftfuns 6231 ofmpteq 6576 qliftfuns 7475 xpf1o 7759 iunfi 7887 iundom2g 8990 lble 10585 rlimcld2 13690 sumeq2ii 13807 summolem3 13828 zsum 13832 fsum 13834 fsumf1o 13837 sumss2 13840 fsumcvg2 13841 fsumadd 13853 isummulc2 13871 fsum2dlem 13879 fsumcom2 13883 fsumshftm 13890 fsum0diag2 13892 fsummulc2 13893 fsum00 13906 fsumabs 13909 fsumrelem 13915 fsumrlim 13919 fsumo1 13920 o1fsum 13921 fsumiun 13929 isumshft 13945 prodeq2ii 14015 prodmolem3 14035 zprod 14039 fprod 14043 fprodf1o 14048 prodss 14049 fprodser 14051 fprodmul 14062 fproddiv 14063 fprodm1s 14072 fprodp1s 14073 fprodabs 14076 fprod2dlem 14082 fprodcom2 14086 fprodefsum 14197 pcmpt 14885 invfuc 15927 dprd2d2 17725 txcnp 20683 ptcnplem 20684 prdsdsf 21430 prdsxmet 21432 fsumcn 21950 ovolfiniun 22502 ovoliunnul 22508 volfiniun 22548 iunmbl 22554 limciun 22897 dvfsumle 23021 dvfsumabs 23023 dvfsumlem1 23026 dvfsumlem3 23028 dvfsumlem4 23029 dvfsumrlim 23031 dvfsumrlim2 23032 dvfsum2 23034 itgsubst 23049 fsumvma 24189 dchrisumlema 24374 dchrisumlem2 24376 dchrisumlem3 24377 chirred 28096 rspcda 28162 sigapildsyslem 29031 voliune 29100 volfiniune 29101 tfisg 30505 ptrest 31983 poimirlem25 32009 poimirlem26 32010 mzpsubst 35634 rabdiophlem2 35689 etransclem48OLD 38184 etransclem48 38185 sge0iunmpt 38297 |
Copyright terms: Public domain | W3C validator |