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	⊢ 𝐴 ∈ V
Assertion	mptrabex	⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↦ 𝐵 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		mptrabex.1	⊢ 𝐴 ∈ V
2	1	rabex	⊢ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ∈ V
3	2	mptex	⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↦ 𝐵 ) ∈ V