Theorem uvtxel1

Description: Characterization of a universal vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 14-Feb-2022)

	Ref	Expression
Hypotheses	uvtxel.v	|- V = ( Vtx ` G )
	isuvtx.e	|- E = ( Edg ` G )
Assertion	uvtxel1	|- ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. k e. ( V \ { N } ) E. e e. E { k , N } C_ e ) )

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	|- V = ( Vtx ` G )
2		isuvtx.e	|- E = ( Edg ` G )
3		sneq	|- ( n = N -> { n } = { N } )
4	3	difeq2d	|- ( n = N -> ( V \ { n } ) = ( V \ { N } ) )
5		preq2	|- ( n = N -> { k , n } = { k , N } )
6	5	sseq1d	|- ( n = N -> ( { k , n } C_ e <-> { k , N } C_ e ) )
7	6	rexbidv	|- ( n = N -> ( E. e e. E { k , n } C_ e <-> E. e e. E { k , N } C_ e ) )
8	4 7	raleqbidv	|- ( n = N -> ( A. k e. ( V \ { n } ) E. e e. E { k , n } C_ e <-> A. k e. ( V \ { N } ) E. e e. E { k , N } C_ e ) )
9	1 2	isuvtx	|- ( UnivVtx ` G ) = { n e. V | A. k e. ( V \ { n } ) E. e e. E { k , n } C_ e }
10	8 9	elrab2	|- ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. k e. ( V \ { N } ) E. e e. E { k , N } C_ e ) )