Description: A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 30-Oct-2020) (Proof shortened by AV, 14-Feb-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | uvtxel.v | |- V = ( Vtx ` G ) |
|
| Assertion | uvtxisvtx | |- ( N e. ( UnivVtx ` G ) -> N e. V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uvtxel.v | |- V = ( Vtx ` G ) |
|
| 2 | 1 | uvtxel | |- ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) ) |
| 3 | 2 | simplbi | |- ( N e. ( UnivVtx ` G ) -> N e. V ) |