Theorem fvdifsupp

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

	Ref	Expression
Hypotheses	fvdifsupp.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	fvdifsupp.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	fvdifsupp.3	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
	fvdifsupp.4	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) )
Assertion	fvdifsupp	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fvdifsupp.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		fvdifsupp.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		fvdifsupp.3	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
4		fvdifsupp.4	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) )
5	4	eldifbd	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝐹 supp 𝑍 ) )
6	4	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7		elsuppfn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
8	1 2 3 7	syl3anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
9	6 8	mpbirand	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) )
10	9	necon2bbid	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) = 𝑍 ↔ ¬ 𝑋 ∈ ( 𝐹 supp 𝑍 ) ) )
11	5 10	mpbird	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑍 )