This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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