Theorem mptexf

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	mptexf.1	⊢ Ⅎ 𝑥 𝐴
	mptexf.2	⊢ 𝐴 ∈ V
Assertion	mptexf	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		mptexf.1	⊢ Ⅎ 𝑥 𝐴
2		mptexf.2	⊢ 𝐴 ∈ V
3	1	mptexgf	⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
4	2 3	ax-mp	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V