This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 ∧ dom 𝐹 ∈ 𝐵 ) → 𝐹 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2		fnex	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ dom 𝐹 ∈ 𝐵 ) → 𝐹 ∈ V )
3	1 2	sylanb	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ) → 𝐹 ∈ V )