Definition df-fusgr 27093

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 27092	. 2 class FinUSGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1532	. . . . 5 class 𝑔
4		cvtx 26775	. . . . 5 class Vtx
5	3, 4	cfv 6349	. . . 4 class (Vtx‘𝑔)
6		cfn 8503	. . . 4 class Fin
7	5, 6	wcel 2110	. . 3 wff (Vtx‘𝑔) ∈ Fin
8		cusgr 26928	. . 3 class USGraph
9	7, 2, 8	crab 3142	. 2 class {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
10	1, 9	wceq 1533	1 wff FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}

This definition is referenced by:  isfusgr  27094