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\to C=E$$
	cbvmpov.2	$$⊢y=w\to E=D$$
Assertion	cbvmpov	$$⊢\left(x\in A,y\in B⟼C\right)=\left(z\in A,w\in B⟼D\right)$$

Proof

Step	Hyp	Ref	Expression
1		cbvmpov.1	$$⊢x=z\to C=E$$
2		cbvmpov.2	$$⊢y=w\to E=D$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}zC$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}wC$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xD$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}yD$$
7	1 2	sylan9eq	$$⊢\left(x=z\wedge y=w\right)\to C=D$$
8	3 4 5 6 7	cbvmpo	$$⊢\left(x\in A,y\in B⟼C\right)=\left(z\in A,w\in B⟼D\right)$$