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 e. W -> <. V , (/) >. e. USGraph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opex | |- <. V , (/) >. e. _V |
|
| 2 | 1 | a1i | |- ( V e. W -> <. V , (/) >. e. _V ) |
| 3 | 0ex | |- (/) e. _V |
|
| 4 | opiedgfv | |- ( ( V e. W /\ (/) e. _V ) -> ( iEdg ` <. V , (/) >. ) = (/) ) |
|
| 5 | 3 4 | mpan2 | |- ( V e. W -> ( iEdg ` <. V , (/) >. ) = (/) ) |
| 6 | 2 5 | usgr0e | |- ( V e. W -> <. V , (/) >. e. USGraph ) |