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\left(B\right)\to B\in \mathrm{dom}F$$

Proof

Step	Hyp	Ref	Expression
1		n0i	$$⊢A\in F\left(B\right)\to \neg F\left(B\right)=\varnothing$$
2		ndmfv	$$⊢\neg B\in \mathrm{dom}F\to F\left(B\right)=\varnothing$$
3	1 2	nsyl2	$$⊢A\in F\left(B\right)\to B\in \mathrm{dom}F$$