Theorem nbgrnself

Description: A vertex in a graph is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 3-Nov-2020) (Revised by AV, 21-Mar-2021)

	Ref	Expression
Hypothesis	nbgrnself.v	|- V = ( Vtx ` G )
Assertion	nbgrnself	|- A. v e. V v e/ ( G NeighbVtx v )

Proof

Step	Hyp	Ref	Expression
1		nbgrnself.v	|- V = ( Vtx ` G )
2		neldifsnd	|- ( v e. V -> -. v e. ( V \ { v } ) )
3	2	intnanrd	|- ( v e. V -> -. ( v e. ( V \ { v } ) /\ E. e e. ( Edg ` G ) { v , v } C_ e ) )
4		df-nel	|- ( v e/ { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } <-> -. v e. { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } )
5		preq2	|- ( n = v -> { v , n } = { v , v } )
6	5	sseq1d	|- ( n = v -> ( { v , n } C_ e <-> { v , v } C_ e ) )
7	6	rexbidv	|- ( n = v -> ( E. e e. ( Edg ` G ) { v , n } C_ e <-> E. e e. ( Edg ` G ) { v , v } C_ e ) )
8	7	elrab	|- ( v e. { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } <-> ( v e. ( V \ { v } ) /\ E. e e. ( Edg ` G ) { v , v } C_ e ) )
9	4 8	xchbinx	|- ( v e/ { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } <-> -. ( v e. ( V \ { v } ) /\ E. e e. ( Edg ` G ) { v , v } C_ e ) )
10	3 9	sylibr	|- ( v e. V -> v e/ { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } )
11		eqidd	|- ( v e. V -> v = v )
12		eqid	|- ( Edg ` G ) = ( Edg ` G )
13	1 12	nbgrval	|- ( v e. V -> ( G NeighbVtx v ) = { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } )
14	11 13	neleq12d	|- ( v e. V -> ( v e/ ( G NeighbVtx v ) <-> v e/ { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } ) )
15	10 14	mpbird	|- ( v e. V -> v e/ ( G NeighbVtx v ) )
16	15	rgen	|- A. v e. V v e/ ( G NeighbVtx v )