Theorem cbvmpt 4357

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 1664	. . . 4
2		nfv 1664	. . . . 5
3		nfs1v 2134	. . . . 5
4	2, 3	nfan 1851	. . . 4
5		eleq1 2482	. . . . 5
6		sbequ12 1927	. . . . 5
7	5, 6	anbi12d 695	. . . 4
8	1, 4, 7	cbvopab1 4337	. . 3
9		nfv 1664	. . . . 5
10		cbvmpt.1	. . . . . . 7
11	10	nfeq2 2569	. . . . . 6
12	11	nfsb 2138	. . . . 5
13	9, 12	nfan 1851	. . . 4
14		nfv 1664	. . . 4
15		eleq1 2482	. . . . 5
16		sbequ 2056	. . . . . 6
17		cbvmpt.2	. . . . . . . 8
18	17	nfeq2 2569	. . . . . . 7
19		cbvmpt.3	. . . . . . . 8
20	19	eqeq2d 2433	. . . . . . 7
21	18, 20	sbie 2090	. . . . . 6
22	16, 21	syl6bb 255	. . . . 5
23	15, 22	anbi12d 695	. . . 4
24	13, 14, 23	cbvopab1 4337	. . 3
25	8, 24	eqtri 2442	. 2
26		df-mpt 4327	. 2
27		df-mpt 4327	. 2
28	25, 26, 27	3eqtr4i 2452	1

Syntax hints:  ->wi 4  /\wa 362  =wceq 1687  [wsb 1693  e.wcel 1749  F/_wnfc 2545  {copab 4324  e.cmpt 4325

This theorem is referenced by:  cbvmptv  4358  dffn5f  5716  fvmpts  5746  fvmpt2i  5750  fvmptex  5754  fmptcof  5846  fmptcos  5847  fliftfuns  5975  offval2  6306  ofmpteq  6308  qliftfuns  7148  axcc2  8553  ac6num  8595  seqof2  11805  summolem2a  13133  zsum  13136  fsumcvg2  13145  fsumrlim  13214  pcmptdvds  13896  prdsdsval2  14362  gsum2d2  16357  dprd2d2  16411  gsumdixp  16525  psrass1lem  17262  madugsum  18153  cnmpt1t  18942  cnmpt2k  18965  elmptrab  19104  flfcnp2  19284  prdsxmet  19644  fsumcn  20146  ovoliunlem3  20687  ovoliun  20688  ovoliun2  20689  voliun  20735  mbfpos  20829  mbfposb  20831  i1fposd  20885  itg2cnlem1  20939  isibl2  20944  cbvitg  20953  itgss3  20992  itgfsum  21004  itgabs  21012  itgcn  21020  limcmpt  21058  dvmptfsum  21147  lhop2  21187  dvfsumle  21193  dvfsumlem2  21199  itgsubstlem  21220  itgsubst  21221  itgulm2  21615  rlimcnp2  22101  gsumconstf  25950  xrge0tmd  26085  cbvprod  27130  prodmolem2a  27149  zprod  27152  fprod  27156  mbfposadd  28110  itgabsnc  28132  ftc1cnnclem  28136  ftc2nc  28147  mzpsubst  28758  rabdiophlem2  28813  aomclem8  29087  fsumcnf  29416  cncfmptss  29441  mulc1cncfg  29444  expcnfg  29447  stoweidlem21  29490  stirlinglem4  29546  stirlinglem13  29555  stirlinglem15  29557  gsumX2d2  30506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403

This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-opab 4326  df-mpt 4327