Metamath Proof Explorer

Theorem setrec2lem1

Description: Lemma for setrec2 . The functional part of F has the same values as F . (Contributed by Emmett Weisz, 4-Mar-2021) (New usage is discouraged.)

Ref Expression
Assertion setrec2lem1 
|- ( ( F |` { x | E! y x F y } ) ` a ) = ( F ` a )

Proof

Step Hyp Ref Expression
1 fvres 
 |-  ( a e. { x | E! y x F y } -> ( ( F |` { x | E! y x F y } ) ` a ) = ( F ` a ) )
2 nfvres 
 |-  ( -. a e. { x | E! y x F y } -> ( ( F |` { x | E! y x F y } ) ` a ) = (/) )
3 vex 
 |-  a e. _V
4 breq1 
 |-  ( x = a -> ( x F y <-> a F y ) )
5 4 eubidv 
 |-  ( x = a -> ( E! y x F y <-> E! y a F y ) )
6 3 5 elab 
 |-  ( a e. { x | E! y x F y } <-> E! y a F y )
7 tz6.12-2 
 |-  ( -. E! y a F y -> ( F ` a ) = (/) )
8 6 7 sylnbi 
 |-  ( -. a e. { x | E! y x F y } -> ( F ` a ) = (/) )
9 2 8 eqtr4d 
 |-  ( -. a e. { x | E! y x F y } -> ( ( F |` { x | E! y x F y } ) ` a ) = ( F ` a ) )
10 1 9 pm2.61i 
 |-  ( ( F |` { x | E! y x F y } ) ` a ) = ( F ` a )