# 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}\in {V}\to \left({x}\in {A}⟼{B}\right)\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 funmpt ${⊢}\mathrm{Fun}\left({x}\in {A}⟼{B}\right)$
2 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
3 2 dmmptss ${⊢}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq {A}$
4 ssexg ${⊢}\left(\mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq {A}\wedge {A}\in {V}\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\in \mathrm{V}$
5 3 4 mpan ${⊢}{A}\in {V}\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\in \mathrm{V}$
6 funex ${⊢}\left(\mathrm{Fun}\left({x}\in {A}⟼{B}\right)\wedge \mathrm{dom}\left({x}\in {A}⟼{B}\right)\in \mathrm{V}\right)\to \left({x}\in {A}⟼{B}\right)\in \mathrm{V}$
7 1 5 6 sylancr ${⊢}{A}\in {V}\to \left({x}\in {A}⟼{B}\right)\in \mathrm{V}$