Metamath Proof Explorer

Theorem uvtx0

Description: There is no universal vertex if there is no vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 30-Oct-2020) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypothesis uvtxel.v 
|- V = ( Vtx ` G )
Assertion uvtx0 
|- ( V = (/) -> ( UnivVtx ` G ) = (/) )

Proof

Step Hyp Ref Expression
1 uvtxel.v 
 |-  V = ( Vtx ` G )
2 1 uvtxval 
 |-  ( UnivVtx ` G ) = { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) }
3 rabeq 
 |-  ( V = (/) -> { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } = { v e. (/) | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } )
4 rab0 
 |-  { v e. (/) | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } = (/)
5 3 4 eqtrdi 
 |-  ( V = (/) -> { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } = (/) )
6 2 5 syl5eq 
 |-  ( V = (/) -> ( UnivVtx ` G ) = (/) )