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}$$