Definition df-fusgr 27587

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 = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}

Detailed syntax breakdown of Definition df-fusgr

Step	Hyp	Ref	Expression
1		cfusgr 27586	. 2 class FinUSGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1538	. . . . 5 class 𝑔
4		cvtx 27269	. . . . 5 class Vtx
5	3, 4	cfv 6418	. . . 4 class (Vtx‘𝑔)
6		cfn 8691	. . . 4 class Fin
7	5, 6	wcel 2108	. . 3 wff (Vtx‘𝑔) ∈ Fin
8		cusgr 27422	. . 3 class USGraph
9	7, 2, 8	crab 3067	. 2 class {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
10	1, 9	wceq 1539	1 wff FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}

This definition is referenced by:  isfusgr  27588