This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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