Metamath Proof Explorer


Theorem bj-imafv

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 F A = G A F A = G A

Proof

Step Hyp Ref Expression
1 eqeq1 F A = G A F A = x G A = x
2 1 abbidv F A = G A x | F A = x = x | G A = x
3 2 unieqd F A = G A x | F A = x = x | G A = x
4 dffv4 F A = x | F A = x
5 dffv4 G A = x | G A = x
6 3 4 5 3eqtr4g F A = G A F A = G A