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 } )