Theorem cbvmpo1

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

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

Proof

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