Definition df-fusgr 40536

Description: Define the class of all finite undirected simple graphs without loops (called "finite simple graphs" in the following). A finite 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 40535	. 2 class FinUSGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1474	. . . . 5 class 𝑔
4		cvtx 25673	. . . . 5 class Vtx
5	3, 4	cfv 5804	. . . 4 class (Vtx‘𝑔)
6		cfn 7841	. . . 4 class Fin
7	5, 6	wcel 1977	. . 3 wff (Vtx‘𝑔) ∈ Fin
8		cusgr 40379	. . 3 class USGraph
9	7, 2, 8	crab 2900	. 2 class {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
10	1, 9	wceq 1475	1 wff FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}

This definition is referenced by:  isfusgr  40537