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