Theorem fvimacnvi

Description: A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007)

	Ref	Expression
Assertion	fvimacnvi	$$⊢\left(\mathrm{Fun}F\wedge A\in F^{-1}\left[B\right]\right)\to F\left(A\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		snssi	$$⊢A\in F^{-1}\left[B\right]\to \left\{A\right\}\subseteq F^{-1}\left[B\right]$$
2		funimass2	$$⊢\left(\mathrm{Fun}F\wedge \left\{A\right\}\subseteq F^{-1}\left[B\right]\right)\to F\left[\left\{A\right\}\right]\subseteq B$$
3	1 2	sylan2	$$⊢\left(\mathrm{Fun}F\wedge A\in F^{-1}\left[B\right]\right)\to F\left[\left\{A\right\}\right]\subseteq B$$
4		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
5	4	snss	$$⊢F\left(A\right)\in B\leftrightarrow \left\{F\left(A\right)\right\}\subseteq B$$
6		cnvimass	$$⊢F^{-1}\left[B\right]\subseteq \mathrm{dom}F$$
7	6	sseli	$$⊢A\in F^{-1}\left[B\right]\to A\in \mathrm{dom}F$$
8		funfn	$$⊢\mathrm{Fun}F\leftrightarrow FFn\mathrm{dom}F$$
9		fnsnfv	$$⊢\left(FFn\mathrm{dom}F\wedge A\in \mathrm{dom}F\right)\to \left\{F\left(A\right)\right\}=F\left[\left\{A\right\}\right]$$
10	8 9	sylanb	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \left\{F\left(A\right)\right\}=F\left[\left\{A\right\}\right]$$
11	7 10	sylan2	$$⊢\left(\mathrm{Fun}F\wedge A\in F^{-1}\left[B\right]\right)\to \left\{F\left(A\right)\right\}=F\left[\left\{A\right\}\right]$$
12	11	sseq1d	$$⊢\left(\mathrm{Fun}F\wedge A\in F^{-1}\left[B\right]\right)\to \left(\left\{F\left(A\right)\right\}\subseteq B\leftrightarrow F\left[\left\{A\right\}\right]\subseteq B\right)$$
13	5 12	bitrid	$$⊢\left(\mathrm{Fun}F\wedge A\in F^{-1}\left[B\right]\right)\to \left(F\left(A\right)\in B\leftrightarrow F\left[\left\{A\right\}\right]\subseteq B\right)$$
14	3 13	mpbird	$$⊢\left(\mathrm{Fun}F\wedge A\in F^{-1}\left[B\right]\right)\to F\left(A\right)\in B$$