Theorem cbvmptfg

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. Usage of this theorem is discouraged because it depends on ax-13 . See cbvmptf for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 11-Sep-2011) (Revised by Thierry Arnoux, 9-Mar-2017) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvmptfg.1	|- F/_ x A
	cbvmptfg.2	|- F/_ y A
	cbvmptfg.3	|- F/_ y B
	cbvmptfg.4	|- F/_ x C
	cbvmptfg.5	|- ( x = y -> B = C )
Assertion	cbvmptfg	|- ( x e. A |-> B ) = ( y e. A |-> C )

Proof

Step	Hyp	Ref	Expression
1		cbvmptfg.1	|- F/_ x A
2		cbvmptfg.2	|- F/_ y A
3		cbvmptfg.3	|- F/_ y B
4		cbvmptfg.4	|- F/_ x C
5		cbvmptfg.5	|- ( x = y -> B = C )
6		nfv	|- F/ w ( x e. A /\ z = B )
7	1	nfcri	|- F/ x w e. A
8		nfs1v	|- F/ x [ w / x ] z = B
9	7 8	nfan	|- F/ x ( w e. A /\ [ w / x ] z = B )
10		eleq1w	|- ( x = w -> ( x e. A <-> w e. A ) )
11		sbequ12	|- ( x = w -> ( z = B <-> [ w / x ] z = B ) )
12	10 11	anbi12d	|- ( x = w -> ( ( x e. A /\ z = B ) <-> ( w e. A /\ [ w / x ] z = B ) ) )
13	6 9 12	cbvopab1g	|- { <. x , z >. | ( x e. A /\ z = B ) } = { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) }
14	2	nfcri	|- F/ y w e. A
15	3	nfeq2	|- F/ y z = B
16	15	nfsb	|- F/ y [ w / x ] z = B
17	14 16	nfan	|- F/ y ( w e. A /\ [ w / x ] z = B )
18		nfv	|- F/ w ( y e. A /\ z = C )
19		eleq1w	|- ( w = y -> ( w e. A <-> y e. A ) )
20		sbequ	|- ( w = y -> ( [ w / x ] z = B <-> [ y / x ] z = B ) )
21	4	nfeq2	|- F/ x z = C
22	5	eqeq2d	|- ( x = y -> ( z = B <-> z = C ) )
23	21 22	sbie	|- ( [ y / x ] z = B <-> z = C )
24	20 23	bitrdi	|- ( w = y -> ( [ w / x ] z = B <-> z = C ) )
25	19 24	anbi12d	|- ( w = y -> ( ( w e. A /\ [ w / x ] z = B ) <-> ( y e. A /\ z = C ) ) )
26	17 18 25	cbvopab1g	|- { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
27	13 26	eqtri	|- { <. x , z >. | ( x e. A /\ z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
28		df-mpt	|- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
29		df-mpt	|- ( y e. A |-> C ) = { <. y , z >. | ( y e. A /\ z = C ) }
30	27 28 29	3eqtr4i	|- ( x e. A |-> B ) = ( y e. A |-> C )