Definition df-fusgr 26664

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 26663	. 2 class FinUSGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1600	. . . . 5 class 𝑔
4		cvtx 26344	. . . . 5 class Vtx
5	3, 4	cfv 6135	. . . 4 class (Vtx‘𝑔)
6		cfn 8241	. . . 4 class Fin
7	5, 6	wcel 2106	. . 3 wff (Vtx‘𝑔) ∈ Fin
8		cusgr 26498	. . 3 class USGraph
9	7, 2, 8	crab 3093	. 2 class {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
10	1, 9	wceq 1601	1 wff FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}

This definition is referenced by:  isfusgr  26665