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 e. _V
Assertion	mptrabex	|- ( x e. { y e. A | ph } |-> B ) e. _V

Proof

Step	Hyp	Ref	Expression
1		mptrabex.1	|- A e. _V
2	1	rabex	|- { y e. A | ph } e. _V
3	2	mptex	|- ( x e. { y e. A | ph } |-> B ) e. _V