Definition df-fusgr

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfusgr	|- FinUSGraph
1		vg	|- g
2		cusgr	|- USGraph
3		cvtx	|- Vtx
4	1	cv	|- g
5	4 3	cfv	|- ( Vtx ` g )
6		cfn	|- Fin
7	5 6	wcel	|- ( Vtx ` g ) e. Fin
8	7 1 2	crab	|- { g e. USGraph | ( Vtx ` g ) e. Fin }
9	0 8	wceq	|- FinUSGraph = { g e. USGraph | ( Vtx ` g ) e. Fin }