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 ⊢ A ∈ V
Assertion mptrabex ⊢ x ∈ y ∈ A | φ ⟼ B ∈ V

Proof

Step Hyp Ref Expression
1 mptrabex.1 ⊢ A ∈ V
2 1 rabex ⊢ y ∈ A | φ ∈ V
3 2 mptex ⊢ x ∈ y ∈ A | φ ⟼ B ∈ V