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