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 e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 usgr0vb 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) )
2 1 biimp3ar 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) -> G e. USGraph )