This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ ∧ k ∈ A ∧ k ≠ W → B = Z
suppsssn.a ⊢ φ → A ∈ V
Assertion suppsssn ⊢ φ → k ∈ A ⟼ B supp Z ⊆ W

Proof

Step Hyp Ref Expression
1 suppsssn.n ⊢ φ ∧ k ∈ A ∧ k ≠ W → B = Z
2 suppsssn.a ⊢ φ → A ∈ V
3 eldifsn ⊢ k ∈ A ∖ W ↔ k ∈ A ∧ k ≠ W
4 1 3expb ⊢ φ ∧ k ∈ A ∧ k ≠ W → B = Z
5 3 4 sylan2b ⊢ φ ∧ k ∈ A ∖ W → B = Z
6 5 2 suppss2 ⊢ φ → k ∈ A ⟼ B supp Z ⊆ W