Metamath Proof Explorer

Theorem usgr0v

Description: The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion usgr0v ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ USGraph

Proof

Step Hyp Ref Expression
1 usgr0vb ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ USGraph ↔ iEdg ⁡ G = ∅
2 1 biimp3ar ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ USGraph