Metamath Proof Explorer


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 A , y B C = z A , w 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 A z A
4 eleq1w y = w y B w B
5 3 4 bi2anan9 x = z y = w x A y B z A w 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 A y B v = C z A w B v = D
9 8 cbvoprab12v x y v | x A y B v = C = z w v | z A w B v = D
10 df-mpo x A , y B C = x y v | x A y B v = C
11 df-mpo z A , w B D = z w v | z A w B v = D
12 9 10 11 3eqtr4i x A , y B C = z A , w B D