Definition df-supp 6470

Description: Define the support of a function against a "zero" value. The support of a function is the subset of its domain which is mapped to a value which is not equal to a designed value called the zero value. Note that this definition uses not equal rather than being in terms of an apartness relation (df-ap 8904 or any other apartness relation), and thus is sometimes called "support" rather than "strong support". It is therefore probably most useful when the function has a codomain which has decidable equality and contains the zero value. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.)

Assertion

Ref	Expression
df-supp	|- supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )

Distinct variable group:   x, i, z

Detailed syntax breakdown of Definition df-supp

Step	Hyp	Ref	Expression
1		csupp 6469	. 2 class supp
2		vx	. . 3 setvar x
3		vz	. . 3 setvar z
4		cvv 2821	. . 3 class _V
5	2	cv 1401	. . . . . 6 class x
6		vi	. . . . . . . 8 setvar i
7	6	cv 1401	. . . . . . 7 class i
8	7	csn 3708	. . . . . 6 class { i }
9	5, 8	cima 4775	. . . . 5 class ( x " { i } )
10	3	cv 1401	. . . . . 6 class z
11	10	csn 3708	. . . . 5 class { z }
12	9, 11	wne 2420	. . . 4 wff ( x " { i } ) =/= { z }
13	5	cdm 4772	. . . 4 class dom x
14	12, 6, 13	crab 2532	. . 3 class { i e. dom x | ( x " { i } ) =/= { z } }
15	2, 3, 4, 4, 14	cmpo 6081	. 2 class ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
16	1, 15	wceq 1402	1 wff supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )

This definition is referenced by:  suppval  6471  funsssuppss  6492  fczsupp0  6493  suppssdc  6494  suppssfvg  6497  suppcofn  6500