Metamath Proof Explorer

Theorem funex

Description: If the domain of a function exists, so does the function. Part of Theorem 4.15(v) of Monk1 p. 46. This theorem is derived using the Axiom of Replacement in the form of fnex . (Note: Any resemblance between F.U.N.E.X. and "Have You Any Eggs" is purely a coincidence originated by Swedish chefs.) (Contributed by NM, 11-Nov-1995)

Ref Expression
Assertion funex Fun F dom F B F V


Step Hyp Ref Expression
1 funfn Fun F F Fn dom F
2 fnex F Fn dom F dom F B F V
3 1 2 sylanb Fun F dom F B F V