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 _xA
cbvmptf.2 _yA
cbvmptf.3 _yB
cbvmptf.4 _xC
cbvmptf.5 x=yB=C
Assertion cbvmptf xAB=yAC

Proof

Step Hyp Ref Expression
1 cbvmptf.1 _xA
2 cbvmptf.2 _yA
3 cbvmptf.3 _yB
4 cbvmptf.4 _xC
5 cbvmptf.5 x=yB=C
6 nfv wxAz=B
7 1 nfcri xwA
8 nfs1v xwxz=B
9 7 8 nfan xwAwxz=B
10 eleq1w x=wxAwA
11 sbequ12 x=wz=Bwxz=B
12 10 11 anbi12d x=wxAz=BwAwxz=B
13 6 9 12 cbvopab1 xz|xAz=B=wz|wAwxz=B
14 2 nfcri ywA
15 3 nfeq2 yz=B
16 15 nfsbv ywxz=B
17 14 16 nfan ywAwxz=B
18 nfv wyAz=C
19 eleq1w w=ywAyA
20 sbequ w=ywxz=Byxz=B
21 4 nfeq2 xz=C
22 5 eqeq2d x=yz=Bz=C
23 21 22 sbiev yxz=Bz=C
24 20 23 bitrdi w=ywxz=Bz=C
25 19 24 anbi12d w=ywAwxz=ByAz=C
26 17 18 25 cbvopab1 wz|wAwxz=B=yz|yAz=C
27 13 26 eqtri xz|xAz=B=yz|yAz=C
28 df-mpt xAB=xz|xAz=B
29 df-mpt yAC=yz|yAz=C
30 27 28 29 3eqtr4i xAB=yAC