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 e. V -> ( x e. A |-> B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		funmpt	|- Fun ( x e. A |-> B )
2		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
3	2	dmmptss	|- dom ( x e. A |-> B ) C_ A
4		ssexg	|- ( ( dom ( x e. A |-> B ) C_ A /\ A e. V ) -> dom ( x e. A |-> B ) e. _V )
5	3 4	mpan	|- ( A e. V -> dom ( x e. A |-> B ) e. _V )
6		funex	|- ( ( Fun ( x e. A |-> B ) /\ dom ( x e. A |-> B ) e. _V ) -> ( x e. A |-> B ) e. _V )
7	1 5 6	sylancr	|- ( A e. V -> ( x e. A |-> B ) e. _V )