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 
|- ( 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 )