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	|- A e. _V
Assertion	fvresex	|- { y | E. x y = ( ( F |` A ) ` x ) } e. _V

Proof

Step	Hyp	Ref	Expression
1		fvresex.1	|- A e. _V
2		ssv	|- A C_ _V
3		resmpt	|- ( A C_ _V -> ( ( z e. _V |-> ( F ` z ) ) |` A ) = ( z e. A |-> ( F ` z ) ) )
4	2 3	ax-mp	|- ( ( z e. _V |-> ( F ` z ) ) |` A ) = ( z e. A |-> ( F ` z ) )
5	4	fveq1i	|- ( ( ( z e. _V |-> ( F ` z ) ) |` A ) ` x ) = ( ( z e. A |-> ( F ` z ) ) ` x )
6		fveq2	|- ( z = x -> ( F ` z ) = ( F ` x ) )
7		eqid	|- ( z e. _V |-> ( F ` z ) ) = ( z e. _V |-> ( F ` z ) )
8		fvex	|- ( F ` x ) e. _V
9	6 7 8	fvmpt	|- ( x e. _V -> ( ( z e. _V |-> ( F ` z ) ) ` x ) = ( F ` x ) )
10	9	elv	|- ( ( z e. _V |-> ( F ` z ) ) ` x ) = ( F ` x )
11		fveqres	|- ( ( ( z e. _V |-> ( F ` z ) ) ` x ) = ( F ` x ) -> ( ( ( z e. _V |-> ( F ` z ) ) |` A ) ` x ) = ( ( F |` A ) ` x ) )
12	10 11	ax-mp	|- ( ( ( z e. _V |-> ( F ` z ) ) |` A ) ` x ) = ( ( F |` A ) ` x )
13	5 12	eqtr3i	|- ( ( z e. A |-> ( F ` z ) ) ` x ) = ( ( F |` A ) ` x )
14	13	eqeq2i	|- ( y = ( ( z e. A |-> ( F ` z ) ) ` x ) <-> y = ( ( F |` A ) ` x ) )
15	14	exbii	|- ( E. x y = ( ( z e. A |-> ( F ` z ) ) ` x ) <-> E. x y = ( ( F |` A ) ` x ) )
16	15	abbii	|- { y | E. x y = ( ( z e. A |-> ( F ` z ) ) ` x ) } = { y | E. x y = ( ( F |` A ) ` x ) }
17	1	mptex	|- ( z e. A |-> ( F ` z ) ) e. _V
18	17	fvclex	|- { y | E. x y = ( ( z e. A |-> ( F ` z ) ) ` x ) } e. _V
19	16 18	eqeltrri	|- { y | E. x y = ( ( F |` A ) ` x ) } e. _V