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		trud	⊢ ( 𝐵 ∈ V → ⊤ )
6	5	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ V → ⊤ )
7		ss2rab	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ { 𝑥 ∈ 𝐴 ∣ ⊤ } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ V → ⊤ ) )
8	6 7	mpbir	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ { 𝑥 ∈ 𝐴 ∣ ⊤ }
9	1	rabtru	⊢ { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴
10	8 9	sseqtri	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ 𝐴
11	4 10	eqsstri	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴
12		ssexg	⊢ ( ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
13	11 12	mpan	⊢ ( 𝐴 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
14		funex	⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
15	2 13 14	sylancr	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )