Theorem imaeqsexv

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

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

Proof

Step	Hyp	Ref	Expression
1		imaeqsex.1	|- ( x = ( F ` y ) -> ( ph <-> ps ) )
2		df-rex	|- ( E. x e. ( F " B ) ph <-> E. x ( x e. ( F " B ) /\ ph ) )
3		fvelimab	|- ( ( F Fn A /\ B C_ A ) -> ( x e. ( F " B ) <-> E. y e. B ( F ` y ) = x ) )
4	3	anbi1d	|- ( ( F Fn A /\ B C_ A ) -> ( ( x e. ( F " B ) /\ ph ) <-> ( E. y e. B ( F ` y ) = x /\ ph ) ) )
5	4	exbidv	|- ( ( F Fn A /\ B C_ A ) -> ( E. x ( x e. ( F " B ) /\ ph ) <-> E. x ( E. y e. B ( F ` y ) = x /\ ph ) ) )
6	2 5	syl5bb	|- ( ( F Fn A /\ B C_ A ) -> ( E. x e. ( F " B ) ph <-> E. x ( E. y e. B ( F ` y ) = x /\ ph ) ) )
7		rexcom4	|- ( E. y e. B E. x ( ( F ` y ) = x /\ ph ) <-> E. x E. y e. B ( ( F ` y ) = x /\ ph ) )
8		eqcom	|- ( ( F ` y ) = x <-> x = ( F ` y ) )
9	8	anbi1i	|- ( ( ( F ` y ) = x /\ ph ) <-> ( x = ( F ` y ) /\ ph ) )
10	9	exbii	|- ( E. x ( ( F ` y ) = x /\ ph ) <-> E. x ( x = ( F ` y ) /\ ph ) )
11		fvex	|- ( F ` y ) e. _V
12	11 1	ceqsexv	|- ( E. x ( x = ( F ` y ) /\ ph ) <-> ps )
13	10 12	bitri	|- ( E. x ( ( F ` y ) = x /\ ph ) <-> ps )
14	13	rexbii	|- ( E. y e. B E. x ( ( F ` y ) = x /\ ph ) <-> E. y e. B ps )
15		r19.41v	|- ( E. y e. B ( ( F ` y ) = x /\ ph ) <-> ( E. y e. B ( F ` y ) = x /\ ph ) )
16	15	exbii	|- ( E. x E. y e. B ( ( F ` y ) = x /\ ph ) <-> E. x ( E. y e. B ( F ` y ) = x /\ ph ) )
17	7 14 16	3bitr3ri	|- ( E. x ( E. y e. B ( F ` y ) = x /\ ph ) <-> E. y e. B ps )
18	6 17	bitrdi	|- ( ( F Fn A /\ B C_ A ) -> ( E. x e. ( F " B ) ph <-> E. y e. B ps ) )