Theorem fnsnfv

Description: Singleton of function value. (Contributed by NM, 22-May-1998) (Proof shortened by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Assertion	fnsnfv	$$⊢\left(FFnA\wedge B\in A\right)\to \left\{F\left(B\right)\right\}=F\left[\left\{B\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		imasng	$$⊢B\in A\to F\left[\left\{B\right\}\right]=\left\{y|BFy\right\}$$
2	1	adantl	$$⊢\left(FFnA\wedge B\in A\right)\to F\left[\left\{B\right\}\right]=\left\{y|BFy\right\}$$
3		velsn	$$⊢y\in \left\{F\left(B\right)\right\}\leftrightarrow y=F\left(B\right)$$
4		eqcom	$$⊢y=F\left(B\right)\leftrightarrow F\left(B\right)=y$$
5	3 4	bitri	$$⊢y\in \left\{F\left(B\right)\right\}\leftrightarrow F\left(B\right)=y$$
6		fnbrfvb	$$⊢\left(FFnA\wedge B\in A\right)\to \left(F\left(B\right)=y\leftrightarrow BFy\right)$$
7	5 6	bitr2id	$$⊢\left(FFnA\wedge B\in A\right)\to \left(BFy\leftrightarrow y\in \left\{F\left(B\right)\right\}\right)$$
8	7	abbi1dv	$$⊢\left(FFnA\wedge B\in A\right)\to \left\{y|BFy\right\}=\left\{F\left(B\right)\right\}$$
9	2 8	eqtr2d	$$⊢\left(FFnA\wedge B\in A\right)\to \left\{F\left(B\right)\right\}=F\left[\left\{B\right\}\right]$$