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 ⊢ ∅ ∈ ComplUSGraph

Proof

Step Hyp Ref Expression
1 usgr0 ⊢ ∅ ∈ USGraph
2 cplgr0 ⊢ ∅ ∈ ComplGraph
3 iscusgr ⊢ ∅ ∈ ComplUSGraph ↔ ∅ ∈ USGraph ∧ ∅ ∈ ComplGraph
4 1 2 3 mpbir2an ⊢ ∅ ∈ ComplUSGraph