Theorem cbvmpt 4084

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 1521	. . . 4 |- F/ w ( x e. A /\ z = B )
2		nfv 1521	. . . . 5 |- F/ x w e. A
3		nfs1v 1932	. . . . 5 |- F/ x [ w / x ] z = B
4	2, 3	nfan 1558	. . . 4 |- F/ x ( w e. A /\ [ w / x ] z = B )
5		eleq1 2233	. . . . 5 |- ( x = w -> ( x e. A <-> w e. A ) )
6		sbequ12 1764	. . . . 5 |- ( x = w -> ( z = B <-> [ w / x ] z = B ) )
7	5, 6	anbi12d 470	. . . 4 |- ( x = w -> ( ( x e. A /\ z = B ) <-> ( w e. A /\ [ w / x ] z = B ) ) )
8	1, 4, 7	cbvopab1 4062	. . 3 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) }
9		nfv 1521	. . . . 5 |- F/ y w e. A
10		cbvmpt.1	. . . . . . 7 |- F/_ y B
11	10	nfeq2 2324	. . . . . 6 |- F/ y z = B
12	11	nfsb 1939	. . . . 5 |- F/ y [ w / x ] z = B
13	9, 12	nfan 1558	. . . 4 |- F/ y ( w e. A /\ [ w / x ] z = B )
14		nfv 1521	. . . 4 |- F/ w ( y e. A /\ z = C )
15		eleq1 2233	. . . . 5 |- ( w = y -> ( w e. A <-> y e. A ) )
16		sbequ 1833	. . . . . 6 |- ( w = y -> ( [ w / x ] z = B <-> [ y / x ] z = B ) )
17		cbvmpt.2	. . . . . . . 8 |- F/_ x C
18	17	nfeq2 2324	. . . . . . 7 |- F/ x z = C
19		cbvmpt.3	. . . . . . . 8 |- ( x = y -> B = C )
20	19	eqeq2d 2182	. . . . . . 7 |- ( x = y -> ( z = B <-> z = C ) )
21	18, 20	sbie 1784	. . . . . 6 |- ( [ y / x ] z = B <-> z = C )
22	16, 21	bitrdi 195	. . . . 5 |- ( w = y -> ( [ w / x ] z = B <-> z = C ) )
23	15, 22	anbi12d 470	. . . 4 |- ( w = y -> ( ( w e. A /\ [ w / x ] z = B ) <-> ( y e. A /\ z = C ) ) )
24	13, 14, 23	cbvopab1 4062	. . 3 |- { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
25	8, 24	eqtri 2191	. 2 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
26		df-mpt 4052	. 2 |- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
27		df-mpt 4052	. 2 |- ( y e. A |-> C ) = { <. y , z >. | ( y e. A /\ z = C ) }
28	25, 26, 27	3eqtr4i 2201	1 |- ( x e. A |-> B ) = ( y e. A |-> C )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348   [wsb 1755   e. wcel 2141   F/_wnfc 2299   {copab 4049   |-> cmpt 4050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-opab 4051  df-mpt 4052

This theorem is referenced by:  cbvmptv  4085  dffn5imf  5551  fvmpts  5574  fvmpt2  5579  mptfvex  5581  fmptcof  5663  fmptcos  5664  fliftfuns  5777  offval2  6076  qliftfuns  6597  cc2  7229  summodclem2a  11344  zsumdc  11347  fsum3cvg2  11357  cbvprod  11521  zproddc  11542  fprodseq  11546  pcmptdvds  12297  cnmpt1t  13079  fsumcncntop  13350  limcmpted  13426