Theorem funfvima2

Description: A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997)

	Ref	Expression
Assertion	funfvima2	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funfvima	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) )
2	1	ex	⊢ ( Fun 𝐹 → ( 𝐵 ∈ dom 𝐹 → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) ) )
3	2	com23	⊢ ( Fun 𝐹 → ( 𝐵 ∈ 𝐴 → ( 𝐵 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) ) )
4	3	a2d	⊢ ( Fun 𝐹 → ( ( 𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹 ) → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) ) )
5		ssel	⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹 ) )
6	4 5	impel	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ 𝐴 ) ) )