Metamath Proof Explorer

Theorem usgr0eop

Description: The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020)

Ref Expression
Assertion usgr0eop ⊢ V ∈ W → V ∅ ∈ USGraph

Proof

Step Hyp Ref Expression
1 opex ⊢ V ∅ ∈ V
2 1 a1i ⊢ V ∈ W → V ∅ ∈ V
3 0ex ⊢ ∅ ∈ V
4 opiedgfv ⊢ V ∈ W ∧ ∅ ∈ V → iEdg ⁡ V ∅ = ∅
5 3 4 mpan2 ⊢ V ∈ W → iEdg ⁡ V ∅ = ∅
6 2 5 usgr0e ⊢ V ∈ W → V ∅ ∈ USGraph