Theorem fncnvima2

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

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

Proof

Step	Hyp	Ref	Expression
1		elpreima	|- ( F Fn A -> ( x e. ( `' F " B ) <-> ( x e. A /\ ( F ` x ) e. B ) ) )
2	1	abbi2dv	|- ( F Fn A -> ( `' F " B ) = { x | ( x e. A /\ ( F ` x ) e. B ) } )
3		df-rab	|- { x e. A | ( F ` x ) e. B } = { x | ( x e. A /\ ( F ` x ) e. B ) }
4	2 3	eqtr4di	|- ( F Fn A -> ( `' F " B ) = { x e. A | ( F ` x ) e. B } )