# Metamath Proof Explorer

## Theorem cbvmpox

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo allows B to be a function of x . (Contributed by NM, 29-Dec-2014)

Ref Expression
Hypotheses cbvmpox.1 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{B}$
cbvmpox.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{D}$
cbvmpox.3 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{C}$
cbvmpox.4 ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{C}$
cbvmpox.5 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{E}$
cbvmpox.6 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{E}$
cbvmpox.7 ${⊢}{x}={z}\to {B}={D}$
cbvmpox.8 ${⊢}\left({x}={z}\wedge {y}={w}\right)\to {C}={E}$
Assertion cbvmpox ${⊢}\left({x}\in {A},{y}\in {B}⟼{C}\right)=\left({z}\in {A},{w}\in {D}⟼{E}\right)$

### Proof

Step Hyp Ref Expression
1 cbvmpox.1 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{B}$
2 cbvmpox.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{D}$
3 cbvmpox.3 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{C}$
4 cbvmpox.4 ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{C}$
5 cbvmpox.5 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{E}$
6 cbvmpox.6 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{E}$
7 cbvmpox.7 ${⊢}{x}={z}\to {B}={D}$
8 cbvmpox.8 ${⊢}\left({x}={z}\wedge {y}={w}\right)\to {C}={E}$
9 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
10 1 nfcri ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
11 9 10 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {B}\right)$
12 3 nfeq2 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{u}={C}$
13 11 12 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {u}={C}\right)$
14 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
15 nfcv ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{B}$
16 15 nfcri ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
17 14 16 nfan ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {B}\right)$
18 4 nfeq2 ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{u}={C}$
19 17 18 nfan ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {u}={C}\right)$
20 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
21 2 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}\in {D}$
22 20 21 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {w}\in {D}\right)$
23 5 nfeq2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{u}={E}$
24 22 23 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {A}\wedge {w}\in {D}\right)\wedge {u}={E}\right)$
25 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {w}\in {D}\right)$
26 6 nfeq2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{u}={E}$
27 25 26 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {A}\wedge {w}\in {D}\right)\wedge {u}={E}\right)$
28 eleq1w ${⊢}{x}={z}\to \left({x}\in {A}↔{z}\in {A}\right)$
29 28 adantr ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({x}\in {A}↔{z}\in {A}\right)$
30 7 eleq2d ${⊢}{x}={z}\to \left({y}\in {B}↔{y}\in {D}\right)$
31 eleq1w ${⊢}{y}={w}\to \left({y}\in {D}↔{w}\in {D}\right)$
32 30 31 sylan9bb ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({y}\in {B}↔{w}\in {D}\right)$
33 29 32 anbi12d ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)↔\left({z}\in {A}\wedge {w}\in {D}\right)\right)$
34 8 eqeq2d ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({u}={C}↔{u}={E}\right)$
35 33 34 anbi12d ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {u}={C}\right)↔\left(\left({z}\in {A}\wedge {w}\in {D}\right)\wedge {u}={E}\right)\right)$
36 13 19 24 27 35 cbvoprab12 ${⊢}\left\{⟨⟨{x},{y}⟩,{u}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {u}={C}\right)\right\}=\left\{⟨⟨{z},{w}⟩,{u}⟩|\left(\left({z}\in {A}\wedge {w}\in {D}\right)\wedge {u}={E}\right)\right\}$
37 df-mpo ${⊢}\left({x}\in {A},{y}\in {B}⟼{C}\right)=\left\{⟨⟨{x},{y}⟩,{u}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {u}={C}\right)\right\}$
38 df-mpo ${⊢}\left({z}\in {A},{w}\in {D}⟼{E}\right)=\left\{⟨⟨{z},{w}⟩,{u}⟩|\left(\left({z}\in {A}\wedge {w}\in {D}\right)\wedge {u}={E}\right)\right\}$
39 36 37 38 3eqtr4i ${⊢}\left({x}\in {A},{y}\in {B}⟼{C}\right)=\left({z}\in {A},{w}\in {D}⟼{E}\right)$