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	|- F/_ x A
	mptexf.2	|- A e. _V
Assertion	mptexf	|- ( x e. A |-> B ) e. _V

Proof

Step	Hyp	Ref	Expression
1		mptexf.1	|- F/_ x A
2		mptexf.2	|- A e. _V
3	1	mptexgf	|- ( A e. _V -> ( x e. A |-> B ) e. _V )
4	2 3	ax-mp	|- ( x e. A |-> B ) e. _V