Theorem suppvalfn

Description: The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 22-Apr-2019)

	Ref	Expression
Assertion	suppvalfn	|- ( ( F Fn X /\ X 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	1	3ad2ant1	|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> Fun F )
3		fnex	|- ( ( F Fn X /\ X e. V ) -> F e. _V )
4	3	3adant3	|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> F e. _V )
5		simp3	|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> Z e. W )
6		suppval1	|- ( ( Fun F /\ F e. _V /\ Z e. W ) -> ( F supp Z ) = { i e. dom F | ( F ` i ) =/= Z } )
7	2 4 5 6	syl3anc	|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( F supp Z ) = { i e. dom F | ( F ` i ) =/= Z } )
8		fndm	|- ( F Fn X -> dom F = X )
9	8	3ad2ant1	|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> dom F = X )
10	9	rabeqdv	|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> { i e. dom F | ( F ` i ) =/= Z } = { i e. X | ( F ` i ) =/= Z } )
11	7 10	eqtrd	|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )