# Metamath Proof Explorer

## Theorem uvtxel

Description: A universal vertex, i.e. an element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 29-Oct-2020) (Revised by AV, 14-Feb-2022)

Ref Expression
Hypothesis uvtxel.v
`|- V = ( Vtx ` G )`
Assertion uvtxel
`|- ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) )`

### Proof

Step Hyp Ref Expression
1 uvtxel.v
` |-  V = ( Vtx ` G )`
2 sneq
` |-  ( v = N -> { v } = { N } )`
3 2 difeq2d
` |-  ( v = N -> ( V \ { v } ) = ( V \ { N } ) )`
4 oveq2
` |-  ( v = N -> ( G NeighbVtx v ) = ( G NeighbVtx N ) )`
5 4 eleq2d
` |-  ( v = N -> ( n e. ( G NeighbVtx v ) <-> n e. ( G NeighbVtx N ) ) )`
6 3 5 raleqbidv
` |-  ( v = N -> ( A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) )`
7 1 uvtxval
` |-  ( UnivVtx ` G ) = { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) }`
8 6 7 elrab2
` |-  ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) )`