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	$⊢ A \in F (B) \to B \in dom F$

Proof

Step	Hyp	Ref	Expression
1		n0i	$⊢ A \in F (B) \to \neg F (B) = \emptyset$
2		ndmfv	$⊢ \neg B \in dom F \to F (B) = \emptyset$
3	1 2	nsyl2	$⊢ A \in F (B) \to B \in dom F$