Theorem fvdifsupp

Description: Function value is zero outside of its support. (Contributed by Thierry Arnoux, 21-Jan-2024)

	Ref	Expression
Hypotheses	fvdifsupp.1	$$⊢\phi \to FFnA$$
	fvdifsupp.2	$$⊢\phi \to A\in V$$
	fvdifsupp.3	$$⊢\phi \to Z\in W$$
	fvdifsupp.4	$$⊢\phi \to X\in \left(A\setminus {supp}_Z\left(F\right)\right)$$
Assertion	fvdifsupp	$$⊢\phi \to F\left(X\right)=Z$$

Proof

Step	Hyp	Ref	Expression
1		fvdifsupp.1	$$⊢\phi \to FFnA$$
2		fvdifsupp.2	$$⊢\phi \to A\in V$$
3		fvdifsupp.3	$$⊢\phi \to Z\in W$$
4		fvdifsupp.4	$$⊢\phi \to X\in \left(A\setminus {supp}_Z\left(F\right)\right)$$
5	4	eldifbd	$$⊢\phi \to \neg X\in {supp}_Z\left(F\right)$$
6	4	eldifad	$$⊢\phi \to X\in A$$
7		elsuppfn	$$⊢\left(FFnA\wedge A\in V\wedge Z\in W\right)\to \left(X\in {supp}_Z\left(F\right)\leftrightarrow \left(X\in A\wedge F\left(X\right)\ne Z\right)\right)$$
8	1 2 3 7	syl3anc	$$⊢\phi \to \left(X\in {supp}_Z\left(F\right)\leftrightarrow \left(X\in A\wedge F\left(X\right)\ne Z\right)\right)$$
9	6 8	mpbirand	$$⊢\phi \to \left(X\in {supp}_Z\left(F\right)\leftrightarrow F\left(X\right)\ne Z\right)$$
10	9	necon2bbid	$$⊢\phi \to \left(F\left(X\right)=Z\leftrightarrow \neg X\in {supp}_Z\left(F\right)\right)$$
11	5 10	mpbird	$$⊢\phi \to F\left(X\right)=Z$$