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

Metamath Proof Explorer

Theorem fvdifsupp

Description: Function value is zero outside of its support. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Hypotheses fvdifsupp.1 ⊢ φ → F Fn A
fvdifsupp.2 ⊢ φ → A ∈ V
fvdifsupp.3 ⊢ φ → Z ∈ W
fvdifsupp.4 ⊢ φ → X ∈ A ∖ supp Z⁡ F
Assertion fvdifsupp ⊢ φ → F ⁡ X = Z

Proof

Step Hyp Ref Expression
1 fvdifsupp.1 ⊢ φ → F Fn A
2 fvdifsupp.2 ⊢ φ → A ∈ V
3 fvdifsupp.3 ⊢ φ → Z ∈ W
4 fvdifsupp.4 ⊢ φ → X ∈ A ∖ supp Z⁡ F
5 4 eldifbd ⊢ φ → ¬ X ∈ supp Z⁡ F
6 4 eldifad ⊢ φ → X ∈ A
7 elsuppfn ⊢ F Fn A ∧ A ∈ V ∧ Z ∈ W → X ∈ supp Z⁡ F ↔ X ∈ A ∧ F ⁡ X ≠ Z
8 1 2 3 7 syl3anc ⊢ φ → X ∈ supp Z⁡ F ↔ X ∈ A ∧ F ⁡ X ≠ Z
9 6 8 mpbirand ⊢ φ → X ∈ supp Z⁡ F ↔ F ⁡ X ≠ Z
10 9 necon2bbid ⊢ φ → F ⁡ X = Z ↔ ¬ X ∈ supp Z⁡ F
11 5 10 mpbird ⊢ φ → F ⁡ X = Z