Metamath Proof Explorer


Theorem cbvmptfg

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. Usage of this theorem is discouraged because it depends on ax-13 . See cbvmptf for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 11-Sep-2011) (Revised by Thierry Arnoux, 9-Mar-2017) (New usage is discouraged.)

Ref Expression
Hypotheses cbvmptfg.1 _ x A
cbvmptfg.2 _ y A
cbvmptfg.3 _ y B
cbvmptfg.4 _ x C
cbvmptfg.5 x = y B = C
Assertion cbvmptfg x A B = y A C

Proof

Step Hyp Ref Expression
1 cbvmptfg.1 _ x A
2 cbvmptfg.2 _ y A
3 cbvmptfg.3 _ y B
4 cbvmptfg.4 _ x C
5 cbvmptfg.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 cbvopab1g 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 nfsb 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 sbie 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 cbvopab1g 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