Theorem mptrabex

Description: If the domain of a function given by maps-to notation is a class abstraction based on a set, the function is a set. (Contributed by AV, 16-Jul-2019) (Revised by AV, 26-Mar-2021)

	Ref	Expression
Hypothesis	mptrabex.1	$$⊢A\in \mathrm{V}$$
Assertion	mptrabex	$$⊢\left(x\in \left\{y\in A|\phi \right\}⟼B\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		mptrabex.1	$$⊢A\in \mathrm{V}$$
2	1	rabex	$$⊢\left\{y\in A|\phi \right\}\in \mathrm{V}$$
3	2	mptex	$$⊢\left(x\in \left\{y\in A|\phi \right\}⟼B\right)\in \mathrm{V}$$