Theorem cbvmpt 4098

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 1528	. . . 4 |- F/ w ( x e. A /\ z = B )
2		nfv 1528	. . . . 5 |- F/ x w e. A
3		nfs1v 1939	. . . . 5 |- F/ x [ w / x ] z = B
4	2, 3	nfan 1565	. . . 4 |- F/ x ( w e. A /\ [ w / x ] z = B )
5		eleq1 2240	. . . . 5 |- ( x = w -> ( x e. A <-> w e. A ) )
6		sbequ12 1771	. . . . 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 4076	. . 3 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) }
9		nfv 1528	. . . . 5 |- F/ y w e. A
10		cbvmpt.1	. . . . . . 7 |- F/_ y B
11	10	nfeq2 2331	. . . . . 6 |- F/ y z = B
12	11	nfsb 1946	. . . . 5 |- F/ y [ w / x ] z = B
13	9, 12	nfan 1565	. . . 4 |- F/ y ( w e. A /\ [ w / x ] z = B )
14		nfv 1528	. . . 4 |- F/ w ( y e. A /\ z = C )
15		eleq1 2240	. . . . 5 |- ( w = y -> ( w e. A <-> y e. A ) )
16		sbequ 1840	. . . . . 6 |- ( w = y -> ( [ w / x ] z = B <-> [ y / x ] z = B ) )
17		cbvmpt.2	. . . . . . . 8 |- F/_ x C
18	17	nfeq2 2331	. . . . . . 7 |- F/ x z = C
19		cbvmpt.3	. . . . . . . 8 |- ( x = y -> B = C )
20	19	eqeq2d 2189	. . . . . . 7 |- ( x = y -> ( z = B <-> z = C ) )
21	18, 20	sbie 1791	. . . . . 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 4076	. . 3 |- { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
25	8, 24	eqtri 2198	. 2 |- { <. x , z >. | ( x e. A /\ z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
26		df-mpt 4066	. 2 |- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
27		df-mpt 4066	. 2 |- ( y e. A |-> C ) = { <. y , z >. | ( y e. A /\ z = C ) }
28	25, 26, 27	3eqtr4i 2208	1 |- ( x e. A |-> B ) = ( y e. A |-> C )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   [wsb 1762   e. wcel 2148   F/_wnfc 2306   {copab 4063   |-> cmpt 4064

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-opab 4065  df-mpt 4066

This theorem is referenced by:  cbvmptv  4099  dffn5imf  5571  fvmpts  5594  fvmpt2  5599  mptfvex  5601  fmptcof  5683  fmptcos  5684  fliftfuns  5798  offval2  6097  qliftfuns  6618  cc2  7265  summodclem2a  11384  zsumdc  11387  fsum3cvg2  11397  cbvprod  11561  zproddc  11582  fprodseq  11586  pcmptdvds  12337  cnmpt1t  13716  fsumcncntop  13987  limcmpted  14063