Metamath Proof Explorer

Theorem nbgr0vtx

Description: In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020)

Ref Expression
Assertion nbgr0vtx 
|- ( ( Vtx ` G ) = (/) -> ( G NeighbVtx K ) = (/) )

Proof

Step Hyp Ref Expression
1 ral0 
 |-  A. n e. (/) -. E. e e. ( Edg ` G ) { K , n } C_ e
2 difeq1 
 |-  ( ( Vtx ` G ) = (/) -> ( ( Vtx ` G ) \ { K } ) = ( (/) \ { K } ) )
3 0dif 
 |-  ( (/) \ { K } ) = (/)
4 2 3 eqtrdi 
 |-  ( ( Vtx ` G ) = (/) -> ( ( Vtx ` G ) \ { K } ) = (/) )
5 4 raleqdv 
 |-  ( ( Vtx ` G ) = (/) -> ( A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e <-> A. n e. (/) -. E. e e. ( Edg ` G ) { K , n } C_ e ) )
6 1 5 mpbiri 
 |-  ( ( Vtx ` G ) = (/) -> A. n e. ( ( Vtx ` G ) \ { K } ) -. E. e e. ( Edg ` G ) { K , n } C_ e )
7 6 nbgr0vtxlem 
 |-  ( ( Vtx ` G ) = (/) -> ( G NeighbVtx K ) = (/) )