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	⊢ Ⅎ 𝑥 𝐴
Assertion	mptexgf	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		mptexgf.a	⊢ Ⅎ 𝑥 𝐴
2		funmpt	⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4	3	dmmpt	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
5		tru	⊢ ⊤
6	5	2a1i	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ V → ⊤ ) )
7	6	ss2rabi	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ { 𝑥 ∈ 𝐴 ∣ ⊤ }
8	1	rabtru	⊢ { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴
9	7 8	sseqtri	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ 𝐴
10	4 9	eqsstri	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴
11		ssexg	⊢ ( ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
12	10 11	mpan	⊢ ( 𝐴 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
13		funex	⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
14	2 12 13	sylancr	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )