# Metamath Proof Explorer

## Theorem cbvmptf

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011) (Revised by Thierry Arnoux, 9-Mar-2017) Add disjoint variable condition to avoid ax-13 . See cbvmptfg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024)

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

### Proof

Step Hyp Ref Expression
1 cbvmptf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 cbvmptf.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
3 cbvmptf.3 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
4 cbvmptf.4 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
5 cbvmptf.5 ${⊢}{x}={y}\to {B}={C}$
6 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {z}={B}\right)$
7 1 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}\in {A}$
8 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{z}={B}$
9 7 8 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({w}\in {A}\wedge \left[{w}/{x}\right]{z}={B}\right)$
10 eleq1w ${⊢}{x}={w}\to \left({x}\in {A}↔{w}\in {A}\right)$
11 sbequ12 ${⊢}{x}={w}\to \left({z}={B}↔\left[{w}/{x}\right]{z}={B}\right)$
12 10 11 anbi12d ${⊢}{x}={w}\to \left(\left({x}\in {A}\wedge {z}={B}\right)↔\left({w}\in {A}\wedge \left[{w}/{x}\right]{z}={B}\right)\right)$
13 6 9 12 cbvopab1 ${⊢}\left\{⟨{x},{z}⟩|\left({x}\in {A}\wedge {z}={B}\right)\right\}=\left\{⟨{w},{z}⟩|\left({w}\in {A}\wedge \left[{w}/{x}\right]{z}={B}\right)\right\}$
14 2 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{w}\in {A}$
15 3 nfeq2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}={B}$
16 15 nfsbv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{z}={B}$
17 14 16 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({w}\in {A}\wedge \left[{w}/{x}\right]{z}={B}\right)$
18 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {z}={C}\right)$
19 eleq1w ${⊢}{w}={y}\to \left({w}\in {A}↔{y}\in {A}\right)$
20 sbequ ${⊢}{w}={y}\to \left(\left[{w}/{x}\right]{z}={B}↔\left[{y}/{x}\right]{z}={B}\right)$
21 4 nfeq2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}={C}$
22 5 eqeq2d ${⊢}{x}={y}\to \left({z}={B}↔{z}={C}\right)$
23 21 22 sbiev ${⊢}\left[{y}/{x}\right]{z}={B}↔{z}={C}$
24 20 23 syl6bb ${⊢}{w}={y}\to \left(\left[{w}/{x}\right]{z}={B}↔{z}={C}\right)$
25 19 24 anbi12d ${⊢}{w}={y}\to \left(\left({w}\in {A}\wedge \left[{w}/{x}\right]{z}={B}\right)↔\left({y}\in {A}\wedge {z}={C}\right)\right)$
26 17 18 25 cbvopab1 ${⊢}\left\{⟨{w},{z}⟩|\left({w}\in {A}\wedge \left[{w}/{x}\right]{z}={B}\right)\right\}=\left\{⟨{y},{z}⟩|\left({y}\in {A}\wedge {z}={C}\right)\right\}$
27 13 26 eqtri ${⊢}\left\{⟨{x},{z}⟩|\left({x}\in {A}\wedge {z}={B}\right)\right\}=\left\{⟨{y},{z}⟩|\left({y}\in {A}\wedge {z}={C}\right)\right\}$
28 df-mpt ${⊢}\left({x}\in {A}⟼{B}\right)=\left\{⟨{x},{z}⟩|\left({x}\in {A}\wedge {z}={B}\right)\right\}$
29 df-mpt ${⊢}\left({y}\in {A}⟼{C}\right)=\left\{⟨{y},{z}⟩|\left({y}\in {A}\wedge {z}={C}\right)\right\}$
30 27 28 29 3eqtr4i ${⊢}\left({x}\in {A}⟼{B}\right)=\left({y}\in {A}⟼{C}\right)$