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 ( ( 𝐹 “ { 𝐴 } ) = ( 𝐺 “ { 𝐴 } ) → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ( ( 𝐹 “ { 𝐴 } ) = ( 𝐺 “ { 𝐴 } ) → ( ( 𝐹 “ { 𝐴 } ) = { 𝑥 } ↔ ( 𝐺 “ { 𝐴 } ) = { 𝑥 } ) )
2 1 abbidv ( ( 𝐹 “ { 𝐴 } ) = ( 𝐺 “ { 𝐴 } ) → { 𝑥 ∣ ( 𝐹 “ { 𝐴 } ) = { 𝑥 } } = { 𝑥 ∣ ( 𝐺 “ { 𝐴 } ) = { 𝑥 } } )
3 2 unieqd ( ( 𝐹 “ { 𝐴 } ) = ( 𝐺 “ { 𝐴 } ) → { 𝑥 ∣ ( 𝐹 “ { 𝐴 } ) = { 𝑥 } } = { 𝑥 ∣ ( 𝐺 “ { 𝐴 } ) = { 𝑥 } } )
4 dffv4 ( 𝐹𝐴 ) = { 𝑥 ∣ ( 𝐹 “ { 𝐴 } ) = { 𝑥 } }
5 dffv4 ( 𝐺𝐴 ) = { 𝑥 ∣ ( 𝐺 “ { 𝐴 } ) = { 𝑥 } }
6 3 4 5 3eqtr4g ( ( 𝐹 “ { 𝐴 } ) = ( 𝐺 “ { 𝐴 } ) → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )