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 )