Metamath Proof Explorer


Theorem usgr0vb

Description: The null graph, with no vertices, is a simple graph iff the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017) (Revised by AV, 16-Oct-2020)

Ref Expression
Assertion usgr0vb GWVtxG=GUSGraphiEdgG=

Proof

Step Hyp Ref Expression
1 usgruhgr GUSGraphGUHGraph
2 uhgr0vb GWVtxG=GUHGraphiEdgG=
3 1 2 syl5ib GWVtxG=GUSGraphiEdgG=
4 simpl GWiEdgG=GW
5 simpr GWiEdgG=iEdgG=
6 4 5 usgr0e GWiEdgG=GUSGraph
7 6 ex GWiEdgG=GUSGraph
8 7 adantr GWVtxG=iEdgG=GUSGraph
9 3 8 impbid GWVtxG=GUSGraphiEdgG=