Metamath Proof Explorer

Theorem cusgr0

Description: The null graph (with no vertices and no edges) represented by the empty set is a complete simple graph. (Contributed by AV, 1-Nov-2020)

		Ref	Expression
	Assertion	cusgr0	$⊢ \emptyset \in ComplUSGraph$

Proof

Step	Hyp	Ref	Expression
1		usgr0	$⊢ \emptyset \in USGraph$
2		cplgr0	$⊢ \emptyset \in ComplGraph$
3		iscusgr	$⊢ \emptyset \in ComplUSGraph \leftrightarrow (\emptyset \in USGraph \land \emptyset \in ComplGraph)$
4	1 2 3	mpbir2an	$⊢ \emptyset \in ComplUSGraph$