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	$$⊢\mathrm{FinUSGraph}=\left\{g\in \mathrm{USGraph}|\mathrm{Vtx}\left(g\right)\in \mathrm{Fin}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfusgr	$$class\mathrm{FinUSGraph}$$
1		vg	$$setvarg$$
2		cusgr	$$class\mathrm{USGraph}$$
3		cvtx	$$class\mathrm{Vtx}$$
4	1	cv	$$setvarg$$
5	4 3	cfv	$$class\mathrm{Vtx}\left(g\right)$$
6		cfn	$$class\mathrm{Fin}$$
7	5 6	wcel	$$wff\mathrm{Vtx}\left(g\right)\in \mathrm{Fin}$$
8	7 1 2	crab	$$class\left\{g\in \mathrm{USGraph}|\mathrm{Vtx}\left(g\right)\in \mathrm{Fin}\right\}$$
9	0 8	wceq	$$wff\mathrm{FinUSGraph}=\left\{g\in \mathrm{USGraph}|\mathrm{Vtx}\left(g\right)\in \mathrm{Fin}\right\}$$