Theorem fniniseg2

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

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

Proof

Step	Hyp	Ref	Expression
1		fncnvima2	$$⊢FFnA\to F^{-1}\left[\left\{B\right\}\right]=\left\{x\in A|F\left(x\right)\in \left\{B\right\}\right\}$$
2		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
3	2	elsn	$$⊢F\left(x\right)\in \left\{B\right\}\leftrightarrow F\left(x\right)=B$$
4	3	rabbii	$$⊢\left\{x\in A|F\left(x\right)\in \left\{B\right\}\right\}=\left\{x\in A|F\left(x\right)=B\right\}$$
5	1 4	eqtrdi	$$⊢FFnA\to F^{-1}\left[\left\{B\right\}\right]=\left\{x\in A|F\left(x\right)=B\right\}$$