Theorem fnimasnd

Description: The image of a function by a singleton whose element is in the domain of the function. (Contributed by Steven Nguyen, 7-Jun-2023)

	Ref	Expression
Hypotheses	fnimasnd.1	$$⊢\phi \to FFnA$$
	fnimasnd.2	$$⊢\phi \to S\in A$$
Assertion	fnimasnd	$$⊢\phi \to F\left[\left\{S\right\}\right]=\left\{F\left(S\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fnimasnd.1	$$⊢\phi \to FFnA$$
2		fnimasnd.2	$$⊢\phi \to S\in A$$
3		fnsnfv	$$⊢\left(FFnA\wedge S\in A\right)\to \left\{F\left(S\right)\right\}=F\left[\left\{S\right\}\right]$$
4	1 2 3	syl2anc	$$⊢\phi \to \left\{F\left(S\right)\right\}=F\left[\left\{S\right\}\right]$$
5	4	eqcomd	$$⊢\phi \to F\left[\left\{S\right\}\right]=\left\{F\left(S\right)\right\}$$