Definition df-fusgr 26209

Description: Define the class of all finite undirected simple graphs without loops (called "finite simple graphs" in the following). A finite simple graph is an undirected simple graph of finite order, i.e. with a finite set of vertices. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.)

Assertion

Ref	Expression
df-fusgr	|- FinUSGraph = { g e. USGraph | (Vtx ` g ) e. Fin }

Detailed syntax breakdown of Definition df-fusgr

Step	Hyp	Ref	Expression
1		cfusgr 26208	. 2 class FinUSGraph
2		vg	. . . . . 6 setvar g
3	2	cv 1482	. . . . 5 class g
4		cvtx 25874	. . . . 5 class Vtx
5	3, 4	cfv 5888	. . . 4 class (Vtx ` g )
6		cfn 7955	. . . 4 class Fin
7	5, 6	wcel 1990	. . 3 wff (Vtx ` g ) e. Fin
8		cusgr 26044	. . 3 class USGraph
9	7, 2, 8	crab 2916	. 2 class { g e. USGraph | (Vtx ` g ) e. Fin }
10	1, 9	wceq 1483	1 wff FinUSGraph = { g e. USGraph | (Vtx ` g ) e. Fin }

This definition is referenced by:  isfusgr  26210