This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Detailed syntax breakdown

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