Theorem cbvmpo

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013)

	Ref	Expression
Hypotheses	cbvmpo.1	$$⊢\underset{\_}{Ⅎ}zC$$
	cbvmpo.2	$$⊢\underset{\_}{Ⅎ}wC$$
	cbvmpo.3	$$⊢\underset{\_}{Ⅎ}xD$$
	cbvmpo.4	$$⊢\underset{\_}{Ⅎ}yD$$
	cbvmpo.5	$$⊢\left(x=z\wedge y=w\right)\to C=D$$
Assertion	cbvmpo	$$⊢\left(x\in A,y\in B⟼C\right)=\left(z\in A,w\in B⟼D\right)$$

Proof

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