Theorem cbvmpt 4124

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 4102	. . 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 4102	. . 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 4092	. 2 |- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
27		df-mpt 4092	. 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 4089   |-> cmpt 4090

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 3157  df-sn 3624  df-pr 3625  df-op 3627  df-opab 4091  df-mpt 4092

This theorem is referenced by:  cbvmptv  4125  dffn5imf  5612  fvmpts  5635  fvmpt2  5641  mptfvex  5643  fmptcof  5725  fmptcos  5726  fliftfuns  5841  offval2  6146  qliftfuns  6673  cc2  7327  summodclem2a  11524  zsumdc  11527  fsum3cvg2  11537  cbvprod  11701  zproddc  11722  fprodseq  11726  pcmptdvds  12483  gsumfzconstf  13412  cnmpt1t  14453  fsumcncntop  14724  limcmpted  14817