Description: If the direct image of a singleton under any of two functions is the same, then the values of these functions at the corresponding point agree. (Contributed by BJ, 18-Mar-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-imafv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 | ||
2 | 1 | abbidv | |
3 | 2 | unieqd | |
4 | dffv4 | ||
5 | dffv4 | ||
6 | 3 4 5 | 3eqtr4g |