This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- F/_ x A
Assertion mptexgf 
|- ( A e. V -> ( x e. A |-> B ) e. _V )

Proof

Step Hyp Ref Expression
1 mptexgf.a 
 |-  F/_ x A
2 funmpt 
 |-  Fun ( x e. A |-> B )
3 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
4 3 dmmpt 
 |-  dom ( x e. A |-> B ) = { x e. A | B e. _V }
5 tru 
 |-  T.
6 5 2a1i 
 |-  ( x e. A -> ( B e. _V -> T. ) )
7 6 ss2rabi 
 |-  { x e. A | B e. _V } C_ { x e. A | T. }
8 1 rabtru 
 |-  { x e. A | T. } = A
9 7 8 sseqtri 
 |-  { x e. A | B e. _V } C_ A
10 4 9 eqsstri 
 |-  dom ( x e. A |-> B ) C_ A
11 ssexg 
 |-  ( ( dom ( x e. A |-> B ) C_ A /\ A e. V ) -> dom ( x e. A |-> B ) e. _V )
12 10 11 mpan 
 |-  ( A e. V -> dom ( x e. A |-> B ) e. _V )
13 funex 
 |-  ( ( Fun ( x e. A |-> B ) /\ dom ( x e. A |-> B ) e. _V ) -> ( x e. A |-> B ) e. _V )
14 2 12 13 sylancr 
 |-  ( A e. V -> ( x e. A |-> B ) e. _V )