Theorem imaeqsalv

Description: Substitute a function value into a universal quantifier over an image. (Contributed by Scott Fenton, 27-Sep-2024)

	Ref	Expression
Hypothesis	imaeqsex.1	|- ( x = ( F ` y ) -> ( ph <-> ps ) )
Assertion	imaeqsalv	|- ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		imaeqsex.1	|- ( x = ( F ` y ) -> ( ph <-> ps ) )
2	1	notbid	|- ( x = ( F ` y ) -> ( -. ph <-> -. ps ) )
3	2	imaeqsexv	|- ( ( F Fn A /\ B C_ A ) -> ( E. x e. ( F " B ) -. ph <-> E. y e. B -. ps ) )
4	3	notbid	|- ( ( F Fn A /\ B C_ A ) -> ( -. E. x e. ( F " B ) -. ph <-> -. E. y e. B -. ps ) )
5		dfral2	|- ( A. x e. ( F " B ) ph <-> -. E. x e. ( F " B ) -. ph )
6		dfral2	|- ( A. y e. B ps <-> -. E. y e. B -. ps )
7	4 5 6	3bitr4g	|- ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) )