Theorem usgr0v

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

	Ref	Expression
Assertion	usgr0v	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )

Proof

Step	Hyp	Ref	Expression
1		usgr0vb	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
2	1	biimp3ar	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )