Theorem ndfatafv2

Description: The alternate function value at a class A if the function is not defined at this set A . (Contributed by AV, 2-Sep-2022)

	Ref	Expression
Assertion	ndfatafv2	$$⊢\neg F\mathrm{defAt}A\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=𝒫\bigcup \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		df-afv2	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)$$
2		iffalse	$$⊢\neg F\mathrm{defAt}A\to if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)=𝒫\bigcup \mathrm{ran}F$$
3	1 2	syl5eq	$$⊢\neg F\mathrm{defAt}A\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=𝒫\bigcup \mathrm{ran}F$$