Theorem afvfvn0fveq

Description: If the function's value at an argument is not the empty set, it equals the value of the alternative function at this argument. (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afvfvn0fveq	$$⊢F\left(A\right)\ne \varnothing \to \left(F\mathrm{\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		afvfundmfveq	$$⊢F\mathrm{defAt}A\to \left(F\mathrm{\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{'}}A\right)=F\left(A\right)$$