Metamath Proof Explorer


Theorem fniniseg2

Description: Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion fniniseg2
|- ( F Fn A -> ( `' F " { B } ) = { x e. A | ( F ` x ) = B } )

Proof

Step Hyp Ref Expression
1 fncnvima2
 |-  ( F Fn A -> ( `' F " { B } ) = { x e. A | ( F ` x ) e. { B } } )
2 fvex
 |-  ( F ` x ) e. _V
3 2 elsn
 |-  ( ( F ` x ) e. { B } <-> ( F ` x ) = B )
4 3 rabbii
 |-  { x e. A | ( F ` x ) e. { B } } = { x e. A | ( F ` x ) = B }
5 1 4 eqtrdi
 |-  ( F Fn A -> ( `' F " { B } ) = { x e. A | ( F ` x ) = B } )