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 _ x A
cbvmptf.2 _ y A
cbvmptf.3 _ y B
cbvmptf.4 _ x C
cbvmptf.5 x = y B = C
Assertion cbvmptf x A B = y A C

Proof

Step Hyp Ref Expression
1 cbvmptf.1 _ x A
2 cbvmptf.2 _ y A
3 cbvmptf.3 _ y B
4 cbvmptf.4 _ x C
5 cbvmptf.5 x = y B = C
6 nfv w x A z = B
7 1 nfcri x w A
8 nfs1v x w x z = B
9 7 8 nfan x w A w x z = B
10 eleq1w x = w x A w A
11 sbequ12 x = w z = B w x z = B
12 10 11 anbi12d x = w x A z = B w A w x z = B
13 6 9 12 cbvopab1 x z | x A z = B = w z | w A w x z = B
14 2 nfcri y w A
15 3 nfeq2 y z = B
16 15 nfsbv y w x z = B
17 14 16 nfan y w A w x z = B
18 nfv w y A z = C
19 eleq1w w = y w A y A
20 sbequ w = y w x z = B y x z = B
21 4 nfeq2 x z = C
22 5 eqeq2d x = y z = B z = C
23 21 22 sbiev y x z = B z = C
24 20 23 bitrdi w = y w x z = B z = C
25 19 24 anbi12d w = y w A w x z = B y A z = C
26 17 18 25 cbvopab1 w z | w A w x z = B = y z | y A z = C
27 13 26 eqtri x z | x A z = B = y z | y A z = C
28 df-mpt x A B = x z | x A z = B
29 df-mpt y A C = y z | y A z = C
30 27 28 29 3eqtr4i x A B = y A C