Theorem dfatsnafv2

Description: Singleton of function value, analogous to fnsnfv . (Contributed by AV, 7-Sep-2022)

	Ref	Expression
Assertion	dfatsnafv2	$$⊢F\mathrm{defAt}A\to \left\{\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\right\}=F\left[\left\{A\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		eqcom	$$⊢y=\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y$$
2		dfatbrafv2b	$$⊢\left(F\mathrm{defAt}A\wedge y\in \mathrm{V}\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y\leftrightarrow AFy\right)$$
3	2	elvd	$$⊢F\mathrm{defAt}A\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y\leftrightarrow AFy\right)$$
4	1 3	bitrid	$$⊢F\mathrm{defAt}A\to \left(y=\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\leftrightarrow AFy\right)$$
5	4	abbidv	$$⊢F\mathrm{defAt}A\to \left\{y|y=\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\right\}=\left\{y|AFy\right\}$$
6		df-sn	$$⊢\left\{\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\right\}=\left\{y|y=\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\right\}$$
7	6	a1i	$$⊢F\mathrm{defAt}A\to \left\{\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\right\}=\left\{y|y=\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\right\}$$
8		dfdfat2	$$⊢F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \exists !xAFx\right)$$
9		imasng	$$⊢A\in \mathrm{dom}F\to F\left[\left\{A\right\}\right]=\left\{y|AFy\right\}$$
10	9	adantr	$$⊢\left(A\in \mathrm{dom}F\wedge \exists !xAFx\right)\to F\left[\left\{A\right\}\right]=\left\{y|AFy\right\}$$
11	8 10	sylbi	$$⊢F\mathrm{defAt}A\to F\left[\left\{A\right\}\right]=\left\{y|AFy\right\}$$
12	5 7 11	3eqtr4d	$$⊢F\mathrm{defAt}A\to \left\{\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\right\}=F\left[\left\{A\right\}\right]$$