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

Metamath Proof Explorer

Theorem elsuppfng

Description: An element of the support of a function with a given domain. This version of elsuppfn assumes F is a set rather than its domain X , avoiding ax-rep . (Contributed by SN, 5-Aug-2024)

Ref Expression
Assertion elsuppfng 
|- ( ( F Fn X /\ F e. V /\ Z e. W ) -> ( S e. ( F supp Z ) <-> ( S e. X /\ ( F ` S ) =/= Z ) ) )

Proof

Step Hyp Ref Expression
1 suppvalfng 
 |-  ( ( F Fn X /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )
2 1 eleq2d 
 |-  ( ( F Fn X /\ F e. V /\ Z e. W ) -> ( S e. ( F supp Z ) <-> S e. { i e. X | ( F ` i ) =/= Z } ) )
3 fveq2 
 |-  ( i = S -> ( F ` i ) = ( F ` S ) )
4 3 neeq1d 
 |-  ( i = S -> ( ( F ` i ) =/= Z <-> ( F ` S ) =/= Z ) )
5 4 elrab 
 |-  ( S e. { i e. X | ( F ` i ) =/= Z } <-> ( S e. X /\ ( F ` S ) =/= Z ) )
6 2 5 bitrdi 
 |-  ( ( F Fn X /\ F e. V /\ Z e. W ) -> ( S e. ( F supp Z ) <-> ( S e. X /\ ( F ` S ) =/= Z ) ) )