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	$$⊢\underset{\_}{Ⅎ}xA$$
	mptexf.2	$$⊢A\in \mathrm{V}$$
Assertion	mptexf	$$⊢\left(x\in A⟼B\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		mptexf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		mptexf.2	$$⊢A\in \mathrm{V}$$
3	1	mptexgf	$$⊢A\in \mathrm{V}\to \left(x\in A⟼B\right)\in \mathrm{V}$$
4	2 3	ax-mp	$$⊢\left(x\in A⟼B\right)\in \mathrm{V}$$