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  5633  fvmpts  5656  fvmpt2  5662  mptfvex  5664  fmptcof  5746  fmptcos  5747  fliftfuns  5866  offval2  6173  qliftfuns  6705  cc2  7378  summodclem2a  11634  zsumdc  11637  fsum3cvg2  11647  cbvprod  11811  zproddc  11832  fprodseq  11836  pcmptdvds  12610  gsumfzconstf  13620  cnmpt1t  14699  fsumcncntop  14981  limcmpted  15077  dvmptfsum  15139