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 ⊢Ⅎ_xA
cbvmptfg.2 ⊢Ⅎ_yA
cbvmptfg.3 ⊢Ⅎ_yB
cbvmptfg.4 ⊢Ⅎ_xC
cbvmptfg.5 ⊢x=y→B=C
Assertion cbvmptfg ⊢x∈A⟼B=y∈A⟼C

Proof

Step Hyp Ref Expression
1 cbvmptfg.1 ⊢Ⅎ_xA
2 cbvmptfg.2 ⊢Ⅎ_yA
3 cbvmptfg.3 ⊢Ⅎ_yB
4 cbvmptfg.4 ⊢Ⅎ_xC
5 cbvmptfg.5 ⊢x=y→B=C
6 nfv ⊢Ⅎwx∈A∧z=B
7 1 nfcri ⊢Ⅎxw∈A
8 nfs1v ⊢Ⅎxwxz=B
9 7 8 nfan ⊢Ⅎxw∈A∧wxz=B
10 eleq1w ⊢x=w→x∈A↔w∈A
11 sbequ12 ⊢x=w→z=B↔wxz=B
12 10 11 anbi12d ⊢x=w→x∈A∧z=B↔w∈A∧wxz=B
13 6 9 12 cbvopab1g ⊢xz|x∈A∧z=B=wz|w∈A∧wxz=B
14 2 nfcri ⊢Ⅎyw∈A
15 3 nfeq2 ⊢Ⅎyz=B
16 15 nfsb ⊢Ⅎywxz=B
17 14 16 nfan ⊢Ⅎyw∈A∧wxz=B
18 nfv ⊢Ⅎwy∈A∧z=C
19 eleq1w ⊢w=y→w∈A↔y∈A
20 sbequ ⊢w=y→wxz=B↔yxz=B
21 4 nfeq2 ⊢Ⅎxz=C
22 5 eqeq2d ⊢x=y→z=B↔z=C
23 21 22 sbie ⊢yxz=B↔z=C
24 20 23 bitrdi ⊢w=y→wxz=B↔z=C
25 19 24 anbi12d ⊢w=y→w∈A∧wxz=B↔y∈A∧z=C
26 17 18 25 cbvopab1g ⊢wz|w∈A∧wxz=B=yz|y∈A∧z=C
27 13 26 eqtri ⊢xz|x∈A∧z=B=yz|y∈A∧z=C
28 df-mpt ⊢x∈A⟼B=xz|x∈A∧z=B
29 df-mpt ⊢y∈A⟼C=yz|y∈A∧z=C
30 27 28 29 3eqtr4i ⊢x∈A⟼B=y∈A⟼C