This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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