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