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		nfcv	|- F/_ z C
4		nfcv	|- F/_ w C
5		nfcv	|- F/_ x D
6		nfcv	|- F/_ y D
7	1 2	sylan9eq	|- ( ( x = z /\ y = w ) -> C = D )
8	3 4 5 6 7	cbvmpo	|- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )