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		trud	|- ( B e. _V -> T. )
6	5	rgenw	|- A. x e. A ( B e. _V -> T. )
7		ss2rab	|- ( { x e. A | B e. _V } C_ { x e. A | T. } <-> A. x e. A ( B e. _V -> T. ) )
8	6 7	mpbir	|- { x e. A | B e. _V } C_ { x e. A | T. }
9	1	rabtru	|- { x e. A | T. } = A
10	8 9	sseqtri	|- { x e. A | B e. _V } C_ A
11	4 10	eqsstri	|- dom ( x e. A |-> B ) C_ A
12		ssexg	|- ( ( dom ( x e. A |-> B ) C_ A /\ A e. V ) -> dom ( x e. A |-> B ) e. _V )
13	11 12	mpan	|- ( A e. V -> dom ( x e. A |-> B ) e. _V )
14		funex	|- ( ( Fun ( x e. A |-> B ) /\ dom ( x e. A |-> B ) e. _V ) -> ( x e. A |-> B ) e. _V )
15	2 13 14	sylancr	|- ( A e. V -> ( x e. A |-> B ) e. _V )