Step |
Hyp |
Ref |
Expression |
1 |
|
nbgrcl.v |
|- V = ( Vtx ` G ) |
2 |
|
df-nbgr |
|- NeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { v } ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) |
3 |
2
|
mpoxeldm |
|- ( N e. ( G NeighbVtx X ) -> ( G e. _V /\ X e. [_ G / g ]_ ( Vtx ` g ) ) ) |
4 |
|
csbfv |
|- [_ G / g ]_ ( Vtx ` g ) = ( Vtx ` G ) |
5 |
4 1
|
eqtr4i |
|- [_ G / g ]_ ( Vtx ` g ) = V |
6 |
5
|
eleq2i |
|- ( X e. [_ G / g ]_ ( Vtx ` g ) <-> X e. V ) |
7 |
6
|
biimpi |
|- ( X e. [_ G / g ]_ ( Vtx ` g ) -> X e. V ) |
8 |
3 7
|
simpl2im |
|- ( N e. ( G NeighbVtx X ) -> X e. V ) |