MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fsupp Unicode version

Definition df-fsupp 7850
Description: Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.)
Assertion
Ref Expression
df-fsupp
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-fsupp
StepHypRef Expression
1 cfsupp 7849 . 2
2 vr . . . . . 6
32cv 1394 . . . . 5
43wfun 5587 . . . 4
5 vz . . . . . . 7
65cv 1394 . . . . . 6
7 csupp 6918 . . . . . 6
83, 6, 7co 6296 . . . . 5
9 cfn 7536 . . . . 5
108, 9wcel 1818 . . . 4
114, 10wa 369 . . 3
1211, 2, 5copab 4509 . 2
131, 12wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  relfsupp  7851  isfsupp  7853
  Copyright terms: Public domain W3C validator