# 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$