Theorem fncnvima2

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

	Ref	Expression
Assertion	fncnvima2	$$⊢FFnA\to F^{-1}\left[B\right]=\left\{x\in A|F\left(x\right)\in B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elpreima	$$⊢FFnA\to \left(x\in F^{-1}\left[B\right]\leftrightarrow \left(x\in A\wedge F\left(x\right)\in B\right)\right)$$
2	1	eqabdv	$$⊢FFnA\to F^{-1}\left[B\right]=\left\{x|\left(x\in A\wedge F\left(x\right)\in B\right)\right\}$$
3		df-rab	$$⊢\left\{x\in A|F\left(x\right)\in B\right\}=\left\{x|\left(x\in A\wedge F\left(x\right)\in B\right)\right\}$$
4	2 3	eqtr4di	$$⊢FFnA\to F^{-1}\left[B\right]=\left\{x\in A|F\left(x\right)\in B\right\}$$