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 } ) -> U. { x | ( F " { A } ) = { x } } = U. { x | ( G " { A } ) = { x } } )
4		dffv4	|- ( F ` A ) = U. { x | ( F " { A } ) = { x } }
5		dffv4	|- ( G ` A ) = U. { x | ( G " { A } ) = { x } }
6	3 4 5	3eqtr4g	|- ( ( F " { A } ) = ( G " { A } ) -> ( F ` A ) = ( G ` A ) )