Metamath Proof Explorer

Theorem mptexg

Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion mptexg ⊢ A ∈ V → x ∈ A ⟼ B ∈ V

Proof

Step Hyp Ref Expression
1 funmpt ⊢ Fun ⁡ x ∈ A ⟼ B
2 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
3 2 dmmptss ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A
4 ssexg ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A ∧ A ∈ V → dom ⁡ x ∈ A ⟼ B ∈ V
5 3 4 mpan ⊢ A ∈ V → dom ⁡ x ∈ A ⟼ B ∈ V
6 funex ⊢ Fun ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ∈ V → x ∈ A ⟼ B ∈ V
7 1 5 6 sylancr ⊢ A ∈ V → x ∈ A ⟼ B ∈ V