Theorem afv2fvn0fveq

Description: If the function's value at an argument is not the empty set, it equals the alternate function value at this argument. (Contributed by AV, 3-Sep-2022)

	Ref	Expression
Assertion	afv2fvn0fveq	$$⊢F\left(A\right)\ne \varnothing \to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvfundmfvn0	$$⊢F\left(A\right)\ne \varnothing \to \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
2		df-dfat	$$⊢F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
3	1 2	sylibr	$$⊢F\left(A\right)\ne \varnothing \to F\mathrm{defAt}A$$
4		dfatafv2eqfv	$$⊢F\mathrm{defAt}A\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$
5	3 4	syl	$$⊢F\left(A\right)\ne \varnothing \to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$