Theorem fvresex

Description: Existence of the class of values of a restricted class. (Contributed by NM, 14-Nov-1995) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypothesis	fvresex.1	⊢ 𝐴 ∈ V
Assertion	fvresex	⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) } ∈ V

Proof

Step	Hyp	Ref	Expression
1		fvresex.1	⊢ 𝐴 ∈ V
2		ssv	⊢ 𝐴 ⊆ V
3		resmpt	⊢ ( 𝐴 ⊆ V → ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
4	2 3	ax-mp	⊢ ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) )
5	4	fveq1i	⊢ ( ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 )
6		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
7		eqid	⊢ ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) = ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) )
8		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
9	6 7 8	fvmpt	⊢ ( 𝑥 ∈ V → ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
10	9	elv	⊢ ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 )
11		fveqres	⊢ ( ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) → ( ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) )
12	10 11	ax-mp	⊢ ( ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 )
13	5 12	eqtr3i	⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 )
14	13	eqeq2i	⊢ ( 𝑦 = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) )
15	14	exbii	⊢ ( ∃ 𝑥 𝑦 = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ∃ 𝑥 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) )
16	15	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) } = { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) }
17	1	mptex	⊢ ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ∈ V
18	17	fvclex	⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) } ∈ V
19	16 18	eqeltrri	⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) } ∈ V