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 F B B dom F


Step Hyp Ref Expression
1 n0i A F B ¬ F B =
2 ndmfv ¬ B dom F F B =
3 1 2 nsyl2 A F B B dom F