Theorem fvdifsupp

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

	Ref	Expression
Hypotheses	fvdifsupp.1	|- ( ph -> F Fn A )
	fvdifsupp.2	|- ( ph -> A e. V )
	fvdifsupp.3	|- ( ph -> Z e. W )
	fvdifsupp.4	|- ( ph -> X e. ( A \ ( F supp Z ) ) )
Assertion	fvdifsupp	|- ( ph -> ( F ` X ) = Z )

Proof

Step	Hyp	Ref	Expression
1		fvdifsupp.1	|- ( ph -> F Fn A )
2		fvdifsupp.2	|- ( ph -> A e. V )
3		fvdifsupp.3	|- ( ph -> Z e. W )
4		fvdifsupp.4	|- ( ph -> X e. ( A \ ( F supp Z ) ) )
5	4	eldifbd	|- ( ph -> -. X e. ( F supp Z ) )
6	4	eldifad	|- ( ph -> X e. A )
7		elsuppfn	|- ( ( F Fn A /\ A e. V /\ Z e. W ) -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
8	1 2 3 7	syl3anc	|- ( ph -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
9	6 8	mpbirand	|- ( ph -> ( X e. ( F supp Z ) <-> ( F ` X ) =/= Z ) )
10	9	necon2bbid	|- ( ph -> ( ( F ` X ) = Z <-> -. X e. ( F supp Z ) ) )
11	5 10	mpbird	|- ( ph -> ( F ` X ) = Z )