Theorem elsuppfn

Description: An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019)

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

Proof

Step	Hyp	Ref	Expression
1		suppvalfn	|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )
2	1	eleq2d	|- ( ( F Fn X /\ X 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	syl6bb	|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( S e. ( F supp Z ) <-> ( S e. X /\ ( F ` S ) =/= Z ) ) )