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

Proof

Step	Hyp	Ref	Expression
1		cbvmpo.1	|- F/_ z C
2		cbvmpo.2	|- F/_ w C
3		cbvmpo.3	|- F/_ x D
4		cbvmpo.4	|- F/_ y D
5		cbvmpo.5	|- ( ( x = z /\ y = w ) -> C = D )
6		nfcv	|- F/_ z B
7		nfcv	|- F/_ x B
8		eqidd	|- ( x = z -> B = B )
9	6 7 1 2 3 4 8 5	cbvmpox	|- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )