Theorem cbvmpo2

Description: Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		cbvmpo2.1	|- F/_ y A
2		cbvmpo2.2	|- F/_ w A
3		cbvmpo2.3	|- F/_ w C
4		cbvmpo2.4	|- F/_ y E
5		cbvmpo2.5	|- ( y = w -> C = E )
6	2	nfcri	|- F/ w x e. A
7		nfcv	|- F/_ w B
8	7	nfcri	|- F/ w y e. B
9	6 8	nfan	|- F/ w ( x e. A /\ y e. B )
10	3	nfeq2	|- F/ w u = C
11	9 10	nfan	|- F/ w ( ( x e. A /\ y e. B ) /\ u = C )
12	1	nfcri	|- F/ y x e. A
13		nfv	|- F/ y w e. B
14	12 13	nfan	|- F/ y ( x e. A /\ w e. B )
15	4	nfeq2	|- F/ y u = E
16	14 15	nfan	|- F/ y ( ( x e. A /\ w e. B ) /\ u = E )
17		eleq1w	|- ( y = w -> ( y e. B <-> w e. B ) )
18	17	anbi2d	|- ( y = w -> ( ( x e. A /\ y e. B ) <-> ( x e. A /\ w e. B ) ) )
19	5	eqeq2d	|- ( y = w -> ( u = C <-> u = E ) )
20	18 19	anbi12d	|- ( y = w -> ( ( ( x e. A /\ y e. B ) /\ u = C ) <-> ( ( x e. A /\ w e. B ) /\ u = E ) ) )
21	11 16 20	cbvoprab2	|- { <. <. x , y >. , u >. | ( ( x e. A /\ y e. B ) /\ u = C ) } = { <. <. x , w >. , u >. | ( ( x e. A /\ w e. B ) /\ u = E ) }
22		df-mpo	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , u >. | ( ( x e. A /\ y e. B ) /\ u = C ) }
23		df-mpo	|- ( x e. A , w e. B |-> E ) = { <. <. x , w >. , u >. | ( ( x e. A /\ w e. B ) /\ u = E ) }
24	21 22 23	3eqtr4i	|- ( x e. A , y e. B |-> C ) = ( x e. A , w e. B |-> E )