Metamath Proof Explorer


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 φkAkWB=Z
suppsssn.a φAV
Assertion suppsssn φkABsuppZW

Proof

Step Hyp Ref Expression
1 suppsssn.n φkAkWB=Z
2 suppsssn.a φAV
3 eldifsn kAWkAkW
4 1 3expb φkAkWB=Z
5 3 4 sylan2b φkAWB=Z
6 5 2 suppss2 φkABsuppZW