Metamath Proof Explorer

Theorem elfvex

Description: If a function value has a member, then the argument is a set. (An artifact of our function value definition.) (Contributed by Mario Carneiro, 6-Nov-2015)

Ref Expression
Assertion elfvex A F B B V


Step Hyp Ref Expression
1 elfvdm A F B B dom F
2 1 elexd A F B B V