Theorem cbvmpt 4138

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 1550	. . . 4 |- F/ w ( x e. A /\ z = B )
2		nfv 1550	. . . . 5 |- F/ x w e. A
3		nfs1v 1966	. . . . 5 |- F/ x [ w / x ] z = B
4	2, 3	nfan 1587	. . . 4 |- F/ x ( w e. A /\ [ w / x ] z = B )
5		eleq1 2267	. . . . 5 |- ( x = w -> ( x e. A <-> w e. A ) )
6		sbequ12 1793	. . . . 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 4116	. . 3 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) }
9		nfv 1550	. . . . 5 |- F/ y w e. A
10		cbvmpt.1	. . . . . . 7 |- F/_ y B
11	10	nfeq2 2359	. . . . . 6 |- F/ y z = B
12	11	nfsb 1973	. . . . 5 |- F/ y [ w / x ] z = B
13	9, 12	nfan 1587	. . . 4 |- F/ y ( w e. A /\ [ w / x ] z = B )
14		nfv 1550	. . . 4 |- F/ w ( y e. A /\ z = C )
15		eleq1 2267	. . . . 5 |- ( w = y -> ( w e. A <-> y e. A ) )
16		sbequ 1862	. . . . . 6 |- ( w = y -> ( [ w / x ] z = B <-> [ y / x ] z = B ) )
17		cbvmpt.2	. . . . . . . 8 |- F/_ x C
18	17	nfeq2 2359	. . . . . . 7 |- F/ x z = C
19		cbvmpt.3	. . . . . . . 8 |- ( x = y -> B = C )
20	19	eqeq2d 2216	. . . . . . 7 |- ( x = y -> ( z = B <-> z = C ) )
21	18, 20	sbie 1813	. . . . . 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 4116	. . 3 |- { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
25	8, 24	eqtri 2225	. 2 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
26		df-mpt 4106	. 2 |- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
27		df-mpt 4106	. 2 |- ( y e. A |-> C ) = { <. y , z >. | ( y e. A /\ z = C ) }
28	25, 26, 27	3eqtr4i 2235	1 |- ( x e. A |-> B ) = ( y e. A |-> C )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1372   [wsb 1784   e. wcel 2175   F/_wnfc 2334   {copab 4103   |-> cmpt 4104

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-opab 4105  df-mpt 4106

This theorem is referenced by:  cbvmptv  4139  dffn5imf  5628  fvmpts  5651  fvmpt2  5657  mptfvex  5659  fmptcof  5741  fmptcos  5742  fliftfuns  5857  offval2  6164  qliftfuns  6696  cc2  7361  summodclem2a  11611  zsumdc  11614  fsum3cvg2  11624  cbvprod  11788  zproddc  11809  fprodseq  11813  pcmptdvds  12587  gsumfzconstf  13596  cnmpt1t  14675  fsumcncntop  14957  limcmpted  15053  dvmptfsum  15115