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 | |
|
cbvmptf.2 | |
||
cbvmptf.3 | |
||
cbvmptf.4 | |
||
cbvmptf.5 | |
||
Assertion | cbvmptf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvmptf.1 | |
|
2 | cbvmptf.2 | |
|
3 | cbvmptf.3 | |
|
4 | cbvmptf.4 | |
|
5 | cbvmptf.5 | |
|
6 | nfv | |
|
7 | 1 | nfcri | |
8 | nfs1v | |
|
9 | 7 8 | nfan | |
10 | eleq1w | |
|
11 | sbequ12 | |
|
12 | 10 11 | anbi12d | |
13 | 6 9 12 | cbvopab1 | |
14 | 2 | nfcri | |
15 | 3 | nfeq2 | |
16 | 15 | nfsbv | |
17 | 14 16 | nfan | |
18 | nfv | |
|
19 | eleq1w | |
|
20 | sbequ | |
|
21 | 4 | nfeq2 | |
22 | 5 | eqeq2d | |
23 | 21 22 | sbiev | |
24 | 20 23 | bitrdi | |
25 | 19 24 | anbi12d | |
26 | 17 18 25 | cbvopab1 | |
27 | 13 26 | eqtri | |
28 | df-mpt | |
|
29 | df-mpt | |
|
30 | 27 28 29 | 3eqtr4i | |