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	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑘 ≠ 𝑊 ) → 𝐵 = 𝑍 )
	suppsssn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	suppsssn	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 ) ⊆ { 𝑊 } )

Proof

Step	Hyp	Ref	Expression
1		suppsssn.n	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑘 ≠ 𝑊 ) → 𝐵 = 𝑍 )
2		suppsssn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		eldifsn	⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑊 } ) ↔ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ≠ 𝑊 ) )
4	1	3expb	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑘 ≠ 𝑊 ) ) → 𝐵 = 𝑍 )
5	3 4	sylan2b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑊 } ) ) → 𝐵 = 𝑍 )
6	5 2	suppss2	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 ) ⊆ { 𝑊 } )