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	|- ( ( ph /\ k e. A /\ k =/= W ) -> B = Z )
	suppsssn.a	|- ( ph -> A e. V )
Assertion	suppsssn	|- ( ph -> ( ( k e. A |-> B ) supp Z ) C_ { W } )

Proof

Step	Hyp	Ref	Expression
1		suppsssn.n	|- ( ( ph /\ k e. A /\ k =/= W ) -> B = Z )
2		suppsssn.a	|- ( ph -> A e. V )
3		eldifsn	|- ( k e. ( A \ { W } ) <-> ( k e. A /\ k =/= W ) )
4	1	3expb	|- ( ( ph /\ ( k e. A /\ k =/= W ) ) -> B = Z )
5	3 4	sylan2b	|- ( ( ph /\ k e. ( A \ { W } ) ) -> B = Z )
6	5 2	suppss2	|- ( ph -> ( ( k e. A |-> B ) supp Z ) C_ { W } )