Theorem cbvmpt 4125

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 1539	. . . 4 |- F/ w ( x e. A /\ z = B )
2		nfv 1539	. . . . 5 |- F/ x w e. A
3		nfs1v 1955	. . . . 5 |- F/ x [ w / x ] z = B
4	2, 3	nfan 1576	. . . 4 |- F/ x ( w e. A /\ [ w / x ] z = B )
5		eleq1 2256	. . . . 5 |- ( x = w -> ( x e. A <-> w e. A ) )
6		sbequ12 1782	. . . . 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 4103	. . 3 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) }
9		nfv 1539	. . . . 5 |- F/ y w e. A
10		cbvmpt.1	. . . . . . 7 |- F/_ y B
11	10	nfeq2 2348	. . . . . 6 |- F/ y z = B
12	11	nfsb 1962	. . . . 5 |- F/ y [ w / x ] z = B
13	9, 12	nfan 1576	. . . 4 |- F/ y ( w e. A /\ [ w / x ] z = B )
14		nfv 1539	. . . 4 |- F/ w ( y e. A /\ z = C )
15		eleq1 2256	. . . . 5 |- ( w = y -> ( w e. A <-> y e. A ) )
16		sbequ 1851	. . . . . 6 |- ( w = y -> ( [ w / x ] z = B <-> [ y / x ] z = B ) )
17		cbvmpt.2	. . . . . . . 8 |- F/_ x C
18	17	nfeq2 2348	. . . . . . 7 |- F/ x z = C
19		cbvmpt.3	. . . . . . . 8 |- ( x = y -> B = C )
20	19	eqeq2d 2205	. . . . . . 7 |- ( x = y -> ( z = B <-> z = C ) )
21	18, 20	sbie 1802	. . . . . 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 4103	. . 3 |- { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
25	8, 24	eqtri 2214	. 2 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
26		df-mpt 4093	. 2 |- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
27		df-mpt 4093	. 2 |- ( y e. A |-> C ) = { <. y , z >. | ( y e. A /\ z = C ) }
28	25, 26, 27	3eqtr4i 2224	1 |- ( x e. A |-> B ) = ( y e. A |-> C )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   [wsb 1773   e. wcel 2164   F/_wnfc 2323   {copab 4090   |-> cmpt 4091

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-opab 4092  df-mpt 4093

This theorem is referenced by:  cbvmptv  4126  dffn5imf  5613  fvmpts  5636  fvmpt2  5642  mptfvex  5644  fmptcof  5726  fmptcos  5727  fliftfuns  5842  offval2  6148  qliftfuns  6675  cc2  7329  summodclem2a  11527  zsumdc  11530  fsum3cvg2  11540  cbvprod  11704  zproddc  11725  fprodseq  11729  pcmptdvds  12486  gsumfzconstf  13415  cnmpt1t  14464  fsumcncntop  14746  limcmpted  14842  dvmptfsum  14904