Metamath Proof Explorer

Theorem mptexgf

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) (Revised by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypothesis mptexgf.a ⊢ Ⅎ _ x A
Assertion mptexgf ⊢ A ∈ V → x ∈ A ⟼ B ∈ V

Proof

Step Hyp Ref Expression
1 mptexgf.a ⊢ Ⅎ _ x A
2 funmpt ⊢ Fun ⁡ x ∈ A ⟼ B
3 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
4 3 dmmpt ⊢ dom ⁡ x ∈ A ⟼ B = x ∈ A | B ∈ V
5 tru ⊢ ⊤
6 5 2a1i ⊢ x ∈ A → B ∈ V → ⊤
7 6 ss2rabi ⊢ x ∈ A | B ∈ V ⊆ x ∈ A | ⊤
8 1 rabtru ⊢ x ∈ A | ⊤ = A
9 7 8 sseqtri ⊢ x ∈ A | B ∈ V ⊆ A
10 4 9 eqsstri ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A
11 ssexg ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A ∧ A ∈ V → dom ⁡ x ∈ A ⟼ B ∈ V
12 10 11 mpan ⊢ A ∈ V → dom ⁡ x ∈ A ⟼ B ∈ V
13 funex ⊢ Fun ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ∈ V → x ∈ A ⟼ B ∈ V
14 2 12 13 sylancr ⊢ A ∈ V → x ∈ A ⟼ B ∈ V