# Metamath Proof Explorer

## Theorem cbvmpo2

Description: Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

### Proof

Step Hyp Ref Expression
1 cbvmpo2.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
2 cbvmpo2.2 ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{A}$
3 cbvmpo2.3 ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{C}$
4 cbvmpo2.4 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{E}$
5 cbvmpo2.5 ${⊢}{y}={w}\to {C}={E}$
6 2 nfcri ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
7 nfcv ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{B}$
8 7 nfcri ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
9 6 8 nfan ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {B}\right)$
10 3 nfeq2 ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{u}={C}$
11 9 10 nfan ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {u}={C}\right)$
12 1 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
13 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{w}\in {B}$
14 12 13 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {w}\in {B}\right)$
15 4 nfeq2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{u}={E}$
16 14 15 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {w}\in {B}\right)\wedge {u}={E}\right)$
17 eleq1w ${⊢}{y}={w}\to \left({y}\in {B}↔{w}\in {B}\right)$
18 17 anbi2d ${⊢}{y}={w}\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)↔\left({x}\in {A}\wedge {w}\in {B}\right)\right)$
19 5 eqeq2d ${⊢}{y}={w}\to \left({u}={C}↔{u}={E}\right)$
20 18 19 anbi12d ${⊢}{y}={w}\to \left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {u}={C}\right)↔\left(\left({x}\in {A}\wedge {w}\in {B}\right)\wedge {u}={E}\right)\right)$
21 11 16 20 cbvoprab2 ${⊢}\left\{⟨⟨{x},{y}⟩,{u}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {u}={C}\right)\right\}=\left\{⟨⟨{x},{w}⟩,{u}⟩|\left(\left({x}\in {A}\wedge {w}\in {B}\right)\wedge {u}={E}\right)\right\}$
22 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\}$
23 df-mpo ${⊢}\left({x}\in {A},{w}\in {B}⟼{E}\right)=\left\{⟨⟨{x},{w}⟩,{u}⟩|\left(\left({x}\in {A}\wedge {w}\in {B}\right)\wedge {u}={E}\right)\right\}$
24 21 22 23 3eqtr4i ${⊢}\left({x}\in {A},{y}\in {B}⟼{C}\right)=\left({x}\in {A},{w}\in {B}⟼{E}\right)$