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	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	funfvima2d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		funfvima2d.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
3		ssidd	⊢ ( 𝜑 → 𝐴 ⊆ 𝐴 )
4	1	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
5	3 4	sseqtrrd	⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
6		funfvima2	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑋 ∈ 𝐴 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐴 ) ) )
7	2 5 6	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐴 ) ) )
8	7	imp	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐴 ) )