Theorem suppvalfng

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

	Ref	Expression
Assertion	suppvalfng	|- ( ( F Fn X /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )

Proof

Step	Hyp	Ref	Expression
1		fnfun	|- ( F Fn X -> Fun F )
2		suppval1	|- ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { i e. dom F | ( F ` i ) =/= Z } )
3	1 2	syl3an1	|- ( ( F Fn X /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { i e. dom F | ( F ` i ) =/= Z } )
4		fndm	|- ( F Fn X -> dom F = X )
5	4	3ad2ant1	|- ( ( F Fn X /\ F e. V /\ Z e. W ) -> dom F = X )
6	5	rabeqdv	|- ( ( F Fn X /\ F e. V /\ Z e. W ) -> { i e. dom F | ( F ` i ) =/= Z } = { i e. X | ( F ` i ) =/= Z } )
7	3 6	eqtrd	|- ( ( F Fn X /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )