Theorem cbvmpox2

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo allows A to be a function of y , analogous to cbvmpox . (Contributed by AV, 30-Mar-2019)

	Ref	Expression
Hypotheses	cbvmpox2.1	|- F/_ z A
	cbvmpox2.2	|- F/_ y D
	cbvmpox2.3	|- F/_ z C
	cbvmpox2.4	|- F/_ w C
	cbvmpox2.5	|- F/_ x E
	cbvmpox2.6	|- F/_ y E
	cbvmpox2.7	|- ( y = z -> A = D )
	cbvmpox2.8	|- ( ( y = z /\ x = w ) -> C = E )
Assertion	cbvmpox2	|- ( x e. A , y e. B |-> C ) = ( w e. D , z e. B |-> E )

Proof

Step	Hyp	Ref	Expression
1		cbvmpox2.1	|- F/_ z A
2		cbvmpox2.2	|- F/_ y D
3		cbvmpox2.3	|- F/_ z C
4		cbvmpox2.4	|- F/_ w C
5		cbvmpox2.5	|- F/_ x E
6		cbvmpox2.6	|- F/_ y E
7		cbvmpox2.7	|- ( y = z -> A = D )
8		cbvmpox2.8	|- ( ( y = z /\ x = w ) -> C = E )
9		nfv	|- F/ w x e. A
10		nfv	|- F/ w y e. B
11	9 10	nfan	|- F/ w ( x e. A /\ y e. B )
12	4	nfeq2	|- F/ w u = C
13	11 12	nfan	|- F/ w ( ( x e. A /\ y e. B ) /\ u = C )
14	1	nfcri	|- F/ z x e. A
15		nfv	|- F/ z y e. B
16	14 15	nfan	|- F/ z ( x e. A /\ y e. B )
17	3	nfeq2	|- F/ z u = C
18	16 17	nfan	|- F/ z ( ( x e. A /\ y e. B ) /\ u = C )
19		nfv	|- F/ x w e. D
20		nfv	|- F/ x z e. B
21	19 20	nfan	|- F/ x ( w e. D /\ z e. B )
22	5	nfeq2	|- F/ x u = E
23	21 22	nfan	|- F/ x ( ( w e. D /\ z e. B ) /\ u = E )
24	2	nfcri	|- F/ y w e. D
25		nfv	|- F/ y z e. B
26	24 25	nfan	|- F/ y ( w e. D /\ z e. B )
27	6	nfeq2	|- F/ y u = E
28	26 27	nfan	|- F/ y ( ( w e. D /\ z e. B ) /\ u = E )
29		eleq1w	|- ( x = w -> ( x e. A <-> w e. A ) )
30	7	eleq2d	|- ( y = z -> ( w e. A <-> w e. D ) )
31	29 30	sylan9bb	|- ( ( x = w /\ y = z ) -> ( x e. A <-> w e. D ) )
32		simpr	|- ( ( x = w /\ y = z ) -> y = z )
33	32	eleq1d	|- ( ( x = w /\ y = z ) -> ( y e. B <-> z e. B ) )
34	31 33	anbi12d	|- ( ( x = w /\ y = z ) -> ( ( x e. A /\ y e. B ) <-> ( w e. D /\ z e. B ) ) )
35	8	ancoms	|- ( ( x = w /\ y = z ) -> C = E )
36	35	eqeq2d	|- ( ( x = w /\ y = z ) -> ( u = C <-> u = E ) )
37	34 36	anbi12d	|- ( ( x = w /\ y = z ) -> ( ( ( x e. A /\ y e. B ) /\ u = C ) <-> ( ( w e. D /\ z e. B ) /\ u = E ) ) )
38	13 18 23 28 37	cbvoprab12	|- { <. <. x , y >. , u >. | ( ( x e. A /\ y e. B ) /\ u = C ) } = { <. <. w , z >. , u >. | ( ( w e. D /\ z e. B ) /\ u = E ) }
39		df-mpo	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , u >. | ( ( x e. A /\ y e. B ) /\ u = C ) }
40		df-mpo	|- ( w e. D , z e. B |-> E ) = { <. <. w , z >. , u >. | ( ( w e. D /\ z e. B ) /\ u = E ) }
41	38 39 40	3eqtr4i	|- ( x e. A , y e. B |-> C ) = ( w e. D , z e. B |-> E )