Theorem cbvmpt 4205

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	|- F/_ y B
cbvmpt.2	|- F/_ x C
cbvmpt.3	|- ( x = y -> B = C )

Assertion

Ref	Expression
cbvmpt	|- ( x e. A |-> B ) = ( y e. A |-> C )

Distinct variable groups:   x, A   y, A

Allowed substitution hints:   B( x, y)   C( x, y)

Proof of Theorem cbvmpt

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

Step	Hyp	Ref	Expression
1		nfv 1577	. . . 4 |- F/ w ( x e. A /\ z = B )
2		nfv 1577	. . . . 5 |- F/ x w e. A
3		nfs1v 1993	. . . . 5 |- F/ x [ w / x ] z = B
4	2, 3	nfan 1614	. . . 4 |- F/ x ( w e. A /\ [ w / x ] z = B )
5		eleq1 2295	. . . . 5 |- ( x = w -> ( x e. A <-> w e. A ) )
6		sbequ12 1820	. . . . 5 |- ( x = w -> ( z = B <-> [ w / x ] z = B ) )
7	5, 6	anbi12d 473	. . . 4 |- ( x = w -> ( ( x e. A /\ z = B ) <-> ( w e. A /\ [ w / x ] z = B ) ) )
8	1, 4, 7	cbvopab1 4183	. . 3 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) }
9		nfv 1577	. . . . 5 |- F/ y w e. A
10		cbvmpt.1	. . . . . . 7 |- F/_ y B
11	10	nfeq2 2396	. . . . . 6 |- F/ y z = B
12	11	nfsb 2000	. . . . 5 |- F/ y [ w / x ] z = B
13	9, 12	nfan 1614	. . . 4 |- F/ y ( w e. A /\ [ w / x ] z = B )
14		nfv 1577	. . . 4 |- F/ w ( y e. A /\ z = C )
15		eleq1 2295	. . . . 5 |- ( w = y -> ( w e. A <-> y e. A ) )
16		sbequ 1889	. . . . . 6 |- ( w = y -> ( [ w / x ] z = B <-> [ y / x ] z = B ) )
17		cbvmpt.2	. . . . . . . 8 |- F/_ x C
18	17	nfeq2 2396	. . . . . . 7 |- F/ x z = C
19		cbvmpt.3	. . . . . . . 8 |- ( x = y -> B = C )
20	19	eqeq2d 2244	. . . . . . 7 |- ( x = y -> ( z = B <-> z = C ) )
21	18, 20	sbie 1840	. . . . . 6 |- ( [ y / x ] z = B <-> z = C )
22	16, 21	bitrdi 196	. . . . 5 |- ( w = y -> ( [ w / x ] z = B <-> z = C ) )
23	15, 22	anbi12d 473	. . . 4 |- ( w = y -> ( ( w e. A /\ [ w / x ] z = B ) <-> ( y e. A /\ z = C ) ) )
24	13, 14, 23	cbvopab1 4183	. . 3 |- { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
25	8, 24	eqtri 2253	. 2 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
26		df-mpt 4173	. 2 |- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
27		df-mpt 4173	. 2 |- ( y e. A |-> C ) = { <. y , z >. | ( y e. A /\ z = C ) }
28	25, 26, 27	3eqtr4i 2263	1 |- ( x e. A |-> B ) = ( y e. A |-> C )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   [wsb 1811   e. wcel 2203   F/_wnfc 2371   {copab 4170   |-> cmpt 4171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-opab 4172  df-mpt 4173

This theorem is referenced by:  cbvmptv  4206  dffn5imf  5732  fvmpts  5755  fvmpt2  5761  mptfvex  5763  fmptcof  5844  fmptcos  5845  fliftfuns  5971  offval2  6282  qliftfuns  6853  cc2  7581  summodclem2a  12067  zsumdc  12070  fsum3cvg2  12080  cbvprod  12244  zproddc  12265  fprodseq  12269  pcmptdvds  13043  gsumfzconstf  14059  cnmpt1t  15150  fsumcncntop  15432  limcmpted  15528  dvmptfsum  15590