![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > cbvmpt | Unicode version |
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.) |
Ref | Expression |
---|---|
cbvmpt.1 | |
cbvmpt.2 | |
cbvmpt.3 |
Ref | Expression |
---|---|
cbvmpt |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1707 | . . . 4 | |
2 | nfv 1707 | . . . . 5 | |
3 | nfs1v 2181 | . . . . 5 | |
4 | 2, 3 | nfan 1928 | . . . 4 |
5 | eleq1 2529 | . . . . 5 | |
6 | sbequ12 1992 | . . . . 5 | |
7 | 5, 6 | anbi12d 710 | . . . 4 |
8 | 1, 4, 7 | cbvopab1 4522 | . . 3 |
9 | nfv 1707 | . . . . 5 | |
10 | cbvmpt.1 | . . . . . . 7 | |
11 | 10 | nfeq2 2636 | . . . . . 6 |
12 | 11 | nfsb 2184 | . . . . 5 |
13 | 9, 12 | nfan 1928 | . . . 4 |
14 | nfv 1707 | . . . 4 | |
15 | eleq1 2529 | . . . . 5 | |
16 | sbequ 2117 | . . . . . 6 | |
17 | cbvmpt.2 | . . . . . . . 8 | |
18 | 17 | nfeq2 2636 | . . . . . . 7 |
19 | cbvmpt.3 | . . . . . . . 8 | |
20 | 19 | eqeq2d 2471 | . . . . . . 7 |
21 | 18, 20 | sbie 2149 | . . . . . 6 |
22 | 16, 21 | syl6bb 261 | . . . . 5 |
23 | 15, 22 | anbi12d 710 | . . . 4 |
24 | 13, 14, 23 | cbvopab1 4522 | . . 3 |
25 | 8, 24 | eqtri 2486 | . 2 |
26 | df-mpt 4512 | . 2 | |
27 | df-mpt 4512 | . 2 | |
28 | 25, 26, 27 | 3eqtr4i 2496 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 /\ wa 369
= wceq 1395 [ wsb 1739 e. wcel 1818
F/_ wnfc 2605
{ copab 4509 e. cmpt 4510 |
This theorem is referenced by: cbvmptv 4543 dffn5f 5928 fvmpts 5958 fvmpt2i 5962 fvmptex 5966 fmptcof 6065 fmptcos 6066 fliftfuns 6212 offval2 6556 ofmpteq 6558 mpt2curryvald 7018 qliftfuns 7417 axcc2 8838 ac6num 8880 seqof2 12165 summolem2a 13537 zsum 13540 fsumcvg2 13549 fsumrlim 13625 cbvprod 13722 prodmolem2a 13741 zprod 13744 fprod 13748 pcmptdvds 14413 prdsdsval2 14881 gsumconstf 16955 gsummpt1n0 16992 gsum2d2 17002 dprd2d2 17093 gsumdixpOLD 17257 gsumdixp 17258 psrass1lem 18029 coe1fzgsumdlem 18343 gsumply1eq 18347 evl1gsumdlem 18392 madugsum 19145 cnmpt1t 20166 cnmpt2k 20189 elmptrab 20328 flfcnp2 20508 prdsxmet 20872 fsumcn 21374 ovoliunlem3 21915 ovoliun 21916 ovoliun2 21917 voliun 21964 mbfpos 22058 mbfposb 22060 i1fposd 22114 itg2cnlem1 22168 isibl2 22173 cbvitg 22182 itgss3 22221 itgfsum 22233 itgabs 22241 itgcn 22249 limcmpt 22287 dvmptfsum 22376 lhop2 22416 dvfsumle 22422 dvfsumlem2 22428 itgsubstlem 22449 itgsubst 22450 itgulm2 22804 rlimcnp2 23296 mbfposadd 30062 itgabsnc 30084 ftc1cnnclem 30088 ftc2nc 30099 mzpsubst 30681 rabdiophlem2 30735 aomclem8 31007 fsumcnf 31396 cncfmptss 31581 mulc1cncfg 31583 expcnfg 31586 icccncfext 31690 cncficcgt0 31691 cncfiooicclem1 31696 fprodcncf 31704 dvmptmulf 31734 iblsplitf 31769 stoweidlem21 31803 stirlinglem4 31859 stirlinglem13 31868 stirlinglem15 31870 fourierd 32005 fourierclimd 32006 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-rab 2816 df-v 3111 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-nul 3785 df-if 3942 df-sn 4030 df-pr 4032 df-op 4036 df-opab 4511 df-mpt 4512 |
Copyright terms: Public domain | W3C validator |