This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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