Theorem cbvmptf

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) (Revised by Thierry Arnoux, 9-Mar-2017) Add disjoint variable condition to avoid ax-13 . See cbvmptfg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvmptf.1	|- F/_ x A
2		cbvmptf.2	|- F/_ y A
3		cbvmptf.3	|- F/_ y B
4		cbvmptf.4	|- F/_ x C
5		cbvmptf.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	cbvopab1	|- { <. 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	nfsbv	|- 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	sbiev	|- ( [ 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	cbvopab1	|- { <. 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 )