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

Metamath Proof Explorer

Theorem elfvdm

Description: If a function value has a member, then the argument belongs to the domain. (An artifact of our function value definition.) (Contributed by NM, 12-Feb-2007) (Proof shortened by BJ, 22-Oct-2022)

		Ref	Expression
	Assertion	elfvdm	⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) → 𝐵 ∈ dom 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) → ¬ ( 𝐹 ‘ 𝐵 ) = ∅ )
2		ndmfv	⊢ ( ¬ 𝐵 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐵 ) = ∅ )
3	1 2	nsyl2	⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) → 𝐵 ∈ dom 𝐹 )