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 ) ) )