Theorem suppsssn

Description: Show that the support of a function is a subset of a singleton. (Contributed by AV, 21-Jul-2019)

	Ref	Expression
Hypotheses	suppsssn.n	$$⊢\left(\phi \wedge k\in A\wedge k\ne W\right)\to B=Z$$
	suppsssn.a	$$⊢\phi \to A\in V$$
Assertion	suppsssn	$$⊢\phi \to \left(k\in A⟼B\right)\mathrm{supp}Z\subseteq \left\{W\right\}$$

Proof

Step	Hyp	Ref	Expression
1		suppsssn.n	$$⊢\left(\phi \wedge k\in A\wedge k\ne W\right)\to B=Z$$
2		suppsssn.a	$$⊢\phi \to A\in V$$
3		eldifsn	$$⊢k\in \left(A\setminus \left\{W\right\}\right)\leftrightarrow \left(k\in A\wedge k\ne W\right)$$
4	1	3expb	$$⊢\left(\phi \wedge \left(k\in A\wedge k\ne W\right)\right)\to B=Z$$
5	3 4	sylan2b	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{W\right\}\right)\right)\to B=Z$$
6	5 2	suppss2	$$⊢\phi \to \left(k\in A⟼B\right)\mathrm{supp}Z\subseteq \left\{W\right\}$$