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 trud ⊢ B ∈ V → ⊤
6 5 rgenw ⊢ ∀ x ∈ A B ∈ V → ⊤
7 ss2rab ⊢ x ∈ A | B ∈ V ⊆ x ∈ A | ⊤ ↔ ∀ x ∈ A B ∈ V → ⊤
8 6 7 mpbir ⊢ x ∈ A | B ∈ V ⊆ x ∈ A | ⊤
9 1 rabtru ⊢ x ∈ A | ⊤ = A
10 8 9 sseqtri ⊢ x ∈ A | B ∈ V ⊆ A
11 4 10 eqsstri ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A
12 ssexg ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A ∧ A ∈ V → dom ⁡ x ∈ A ⟼ B ∈ V
13 11 12 mpan ⊢ A ∈ V → dom ⁡ x ∈ A ⟼ B ∈ V
14 funex ⊢ Fun ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ∈ V → x ∈ A ⟼ B ∈ V
15 2 13 14 sylancr ⊢ A ∈ V → x ∈ A ⟼ B ∈ V