Theorem cbvmpov

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt , some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypotheses	cbvmpov.1	|- ( x = z -> C = E )
	cbvmpov.2	|- ( y = w -> E = D )
Assertion	cbvmpov	|- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )

Proof

Step	Hyp	Ref	Expression
1		cbvmpov.1	|- ( x = z -> C = E )
2		cbvmpov.2	|- ( y = w -> E = D )
3		eleq1w	|- ( x = z -> ( x e. A <-> z e. A ) )
4		eleq1w	|- ( y = w -> ( y e. B <-> w e. B ) )
5	3 4	bi2anan9	|- ( ( x = z /\ y = w ) -> ( ( x e. A /\ y e. B ) <-> ( z e. A /\ w e. B ) ) )
6	1 2	sylan9eq	|- ( ( x = z /\ y = w ) -> C = D )
7	6	eqeq2d	|- ( ( x = z /\ y = w ) -> ( v = C <-> v = D ) )
8	5 7	anbi12d	|- ( ( x = z /\ y = w ) -> ( ( ( x e. A /\ y e. B ) /\ v = C ) <-> ( ( z e. A /\ w e. B ) /\ v = D ) ) )
9	8	cbvoprab12v	|- { <. <. x , y >. , v >. | ( ( x e. A /\ y e. B ) /\ v = C ) } = { <. <. z , w >. , v >. | ( ( z e. A /\ w e. B ) /\ v = D ) }
10		df-mpo	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , v >. | ( ( x e. A /\ y e. B ) /\ v = C ) }
11		df-mpo	|- ( z e. A , w e. B |-> D ) = { <. <. z , w >. , v >. | ( ( z e. A /\ w e. B ) /\ v = D ) }
12	9 10 11	3eqtr4i	|- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )