Theorem elsuppfnd

Description: Deduce membership in the support of a function. (Contributed by Thierry Arnoux, 5-Oct-2025)

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

Proof

Step	Hyp	Ref	Expression
1		elsuppfnd.1	$$⊢\phi \to FFnA$$
2		elsuppfnd.2	$$⊢\phi \to A\in V$$
3		elsuppfnd.3	$$⊢\phi \to Z\in W$$
4		elsuppfnd.4	$$⊢\phi \to X\in A$$
5		elsuppfnd.5	$$⊢\phi \to F\left(X\right)\ne Z$$
6		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)$$
7	6	biimpar	$$⊢\left(\left(FFnA\wedge A\in V\wedge Z\in W\right)\wedge \left(X\in A\wedge F\left(X\right)\ne Z\right)\right)\to X\in {supp}_Z\left(F\right)$$
8	1 2 3 4 5 7	syl32anc	$$⊢\phi \to X\in {supp}_Z\left(F\right)$$