Theorem funfvima2d

Description: A function's value in a preimage belongs to the image. (Contributed by Stanislas Polu, 9-Mar-2020) (Revised by AV, 23-Mar-2024)

	Ref	Expression
Hypothesis	funfvima2d.1	|- ( ph -> F : A --> B )
Assertion	funfvima2d	|- ( ( ph /\ X e. A ) -> ( F ` X ) e. ( F " A ) )

Proof

Step	Hyp	Ref	Expression
1		funfvima2d.1	|- ( ph -> F : A --> B )
2	1	ffund	|- ( ph -> Fun F )
3		ssidd	|- ( ph -> A C_ A )
4	1	fdmd	|- ( ph -> dom F = A )
5	3 4	sseqtrrd	|- ( ph -> A C_ dom F )
6		funfvima2	|- ( ( Fun F /\ A C_ dom F ) -> ( X e. A -> ( F ` X ) e. ( F " A ) ) )
7	2 5 6	syl2anc	|- ( ph -> ( X e. A -> ( F ` X ) e. ( F " A ) ) )
8	7	imp	|- ( ( ph /\ X e. A ) -> ( F ` X ) e. ( F " A ) )