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	⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ∅ ⟩ ∈ USGraph )

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ 𝑉 , ∅ ⟩ ∈ V
2	1	a1i	⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ∅ ⟩ ∈ V )
3		0ex	⊢ ∅ ∈ V
4		opiedgfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ∅ ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ∅ ⟩ ) = ∅ )
5	3 4	mpan2	⊢ ( 𝑉 ∈ 𝑊 → ( iEdg ‘ ⟨ 𝑉 , ∅ ⟩ ) = ∅ )
6	2 5	usgr0e	⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ∅ ⟩ ∈ USGraph )