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