Theorem uvtxusgr

Description: The set of all universal vertices of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 31-Oct-2020)

	Ref	Expression
Hypotheses	uvtxnbgr.v	|- V = ( Vtx ` G )
	uvtxusgr.e	|- E = ( Edg ` G )
Assertion	uvtxusgr	|- ( G e. USGraph -> ( UnivVtx ` G ) = { n e. V | A. k e. ( V \ { n } ) { k , n } e. E } )

Proof

Step	Hyp	Ref	Expression
1		uvtxnbgr.v	|- V = ( Vtx ` G )
2		uvtxusgr.e	|- E = ( Edg ` G )
3	1	uvtxval	|- ( UnivVtx ` G ) = { n e. V | A. k e. ( V \ { n } ) k e. ( G NeighbVtx n ) }
4	2	nbusgreledg	|- ( G e. USGraph -> ( k e. ( G NeighbVtx n ) <-> { k , n } e. E ) )
5	4	ralbidv	|- ( G e. USGraph -> ( A. k e. ( V \ { n } ) k e. ( G NeighbVtx n ) <-> A. k e. ( V \ { n } ) { k , n } e. E ) )
6	5	rabbidv	|- ( G e. USGraph -> { n e. V | A. k e. ( V \ { n } ) k e. ( G NeighbVtx n ) } = { n e. V | A. k e. ( V \ { n } ) { k , n } e. E } )
7	3 6	syl5eq	|- ( G e. USGraph -> ( UnivVtx ` G ) = { n e. V | A. k e. ( V \ { n } ) { k , n } e. E } )