Definition df-sgra 10781

Description: Define the class of all simple graphs (pseudographs whose edges connect exactly two vertices each). Definition in [Diestel] p. 2, which simply calls them "graphs".

Assertion

Ref	Expression
df-sgra	|- SmpGrph = {<.a, b>. | ((a i^i b) = (/) /\ b (_ (a ^m 2o))}

Distinct variable group:   a,b

Detailed syntax breakdown of Definition df-sgra

Step	Hyp	Ref	Expression
1		csgra 10780	. 2 class SmpGrph
2		va	. . . . . . 7 set a
3	2	cv 955	. . . . . 6 class a
4		vb	. . . . . . 7 set b
5	4	cv 955	. . . . . 6 class b
6	3, 5	cin 2046	. . . . 5 class (a i^i b)
7		c0 2280	. . . . 5 class (/)
8	6, 7	wceq 956	. . . 4 wff (a i^i b) = (/)
9		c2o 4129	. . . . . 6 class 2o
10		cm 4322	. . . . . 6 class ^m
11	3, 9, 10	co 3963	. . . . 5 class (a ^m 2o)
12	5, 11	wss 2047	. . . 4 wff b (_ (a ^m 2o)
13	8, 12	wa 223	. . 3 wff ((a i^i b) = (/) /\ b (_ (a ^m 2o))
14	13, 2, 4	copab 2666	. 2 class {<.a, b>. | ((a i^i b) = (/) /\ b (_ (a ^m 2o))}
15	1, 14	wceq 956	1 wff SmpGrph = {<.a, b>. | ((a i^i b) = (/) /\ b (_ (a ^m 2o))}

Copyright terms: Public domain