Metamath Proof Explorer


Theorem nbgrnvtx0

Description: If a class X is not a vertex of a graph G , then it has no neighbors in G . (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Hypothesis nbgrel.v V=VtxG
Assertion nbgrnvtx0 XVGNeighbVtxX=

Proof

Step Hyp Ref Expression
1 nbgrel.v V=VtxG
2 csbfv G/gVtxg=VtxG
3 1 2 eqtr4i V=G/gVtxg
4 neleq2 V=G/gVtxgXVXG/gVtxg
5 3 4 ax-mp XVXG/gVtxg
6 5 biimpi XVXG/gVtxg
7 6 olcd XVGVXG/gVtxg
8 df-nbgr NeighbVtx=gV,vVtxgnVtxgv|eEdggvne
9 8 mpoxneldm GVXG/gVtxgGNeighbVtxX=
10 7 9 syl XVGNeighbVtxX=