Theorem uvtxusgrel

Description: A universal vertex, i.e. an element of 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	uvtxusgrel	|- ( G e. USGraph -> ( N e. ( 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 2	uvtxusgr	|- ( G e. USGraph -> ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) { k , v } e. E } )
4	3	eleq2d	|- ( G e. USGraph -> ( N e. ( UnivVtx ` G ) <-> N e. { v e. V | A. k e. ( V \ { v } ) { k , v } e. E } ) )
5		sneq	|- ( v = N -> { v } = { N } )
6	5	difeq2d	|- ( v = N -> ( V \ { v } ) = ( V \ { N } ) )
7		preq2	|- ( v = N -> { k , v } = { k , N } )
8	7	eleq1d	|- ( v = N -> ( { k , v } e. E <-> { k , N } e. E ) )
9	6 8	raleqbidv	|- ( v = N -> ( A. k e. ( V \ { v } ) { k , v } e. E <-> A. k e. ( V \ { N } ) { k , N } e. E ) )
10	9	elrab	|- ( N e. { v e. V | A. k e. ( V \ { v } ) { k , v } e. E } <-> ( N e. V /\ A. k e. ( V \ { N } ) { k , N } e. E ) )
11	4 10	bitrdi	|- ( G e. USGraph -> ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. k e. ( V \ { N } ) { k , N } e. E ) ) )