Theorem cbvmpt 4542

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.)

Hypotheses

Ref	Expression
cbvmpt.1
cbvmpt.2
cbvmpt.3

Assertion

Ref	Expression
cbvmpt

Distinct variable groups:   ,   ,

Proof of Theorem cbvmpt

Dummy variables are mutually distinct and distinct from all other variables.

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

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