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 2917 | . 2 | |
2 | nfcv 2764 | . . . 4 | |
3 | nfv 1843 | . . . . 5 | |
4 | rspc.1 | . . . . 5 | |
5 | 3, 4 | nfim 1825 | . . . 4 |
6 | eleq1 2689 | . . . . 5 | |
7 | rspc.2 | . . . . 5 | |
8 | 6, 7 | imbi12d 334 | . . . 4 |
9 | 2, 5, 8 | spcgf 3288 | . . 3 |
10 | 9 | pm2.43a 54 | . 2 |
11 | 1, 10 | syl5bi 232 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wal 1481 wceq 1483 wnf 1708 wcel 1990 wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-v 3202 |
This theorem is referenced by: rspcv 3305 rspc2 3320 disjxiun 4649 disjxiunOLD 4650 pofun 5051 fmptcof 6397 fliftfuns 6564 ofmpteq 6916 qliftfuns 7834 xpf1o 8122 iunfi 8254 iundom2g 9362 lble 10975 rlimcld2 14309 sumeq2ii 14423 summolem3 14445 zsum 14449 fsum 14451 fsumf1o 14454 sumss2 14457 fsumcvg2 14458 fsumadd 14470 isummulc2 14493 fsum2dlem 14501 fsumcom2 14505 fsumcom2OLD 14506 fsumshftm 14513 fsum0diag2 14515 fsummulc2 14516 fsum00 14530 fsumabs 14533 fsumrelem 14539 fsumrlim 14543 fsumo1 14544 o1fsum 14545 fsumiun 14553 isumshft 14571 prodeq2ii 14643 prodmolem3 14663 zprod 14667 fprod 14671 fprodf1o 14676 prodss 14677 fprodser 14679 fprodmul 14690 fproddiv 14691 fprodm1s 14700 fprodp1s 14701 fprodabs 14704 fprod2dlem 14710 fprodcom2 14714 fprodcom2OLD 14715 fprodefsum 14825 sumeven 15110 sumodd 15111 pcmpt 15596 invfuc 16634 dprd2d2 18443 txcnp 21423 ptcnplem 21424 prdsdsf 22172 prdsxmet 22174 fsumcn 22673 ovolfiniun 23269 ovoliunnul 23275 volfiniun 23315 iunmbl 23321 limciun 23658 dvfsumle 23784 dvfsumabs 23786 dvfsumlem1 23789 dvfsumlem3 23791 dvfsumlem4 23792 dvfsumrlim 23794 dvfsumrlim2 23795 dvfsum2 23797 itgsubst 23812 fsumvma 24938 dchrisumlema 25177 dchrisumlem2 25179 dchrisumlem3 25180 rspc2vd 27129 chirred 29254 fsumiunle 29575 sigapildsyslem 30224 voliune 30292 volfiniune 30293 tfisg 31716 nosupbnd1 31860 ptrest 33408 poimirlem25 33434 poimirlem26 33435 mzpsubst 37311 rabdiophlem2 37366 etransclem48 40499 sge0iunmpt 40635 |
Copyright terms: Public domain | W3C validator |