Theorem nbusgreledg

Description: A class/vertex is a neighbor of another class/vertex in a simple graph iff the vertices are endpoints of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017) (Revised by AV, 26-Oct-2020)

	Ref	Expression
Hypothesis	nbusgreledg.e	|- E = ( Edg ` G )
Assertion	nbusgreledg	|- ( G e. USGraph -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		nbusgreledg.e	|- E = ( Edg ` G )
2		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
3	2 1	nbusgr	|- ( G e. USGraph -> ( G NeighbVtx K ) = { n e. ( Vtx ` G ) | { K , n } e. E } )
4	3	eleq2d	|- ( G e. USGraph -> ( N e. ( G NeighbVtx K ) <-> N e. { n e. ( Vtx ` G ) | { K , n } e. E } ) )
5	1 2	usgrpredgv	|- ( ( G e. USGraph /\ { K , N } e. E ) -> ( K e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) )
6	5	simprd	|- ( ( G e. USGraph /\ { K , N } e. E ) -> N e. ( Vtx ` G ) )
7	6	ex	|- ( G e. USGraph -> ( { K , N } e. E -> N e. ( Vtx ` G ) ) )
8	7	pm4.71rd	|- ( G e. USGraph -> ( { K , N } e. E <-> ( N e. ( Vtx ` G ) /\ { K , N } e. E ) ) )
9		prcom	|- { N , K } = { K , N }
10	9	eleq1i	|- ( { N , K } e. E <-> { K , N } e. E )
11	10	a1i	|- ( G e. USGraph -> ( { N , K } e. E <-> { K , N } e. E ) )
12		preq2	|- ( n = N -> { K , n } = { K , N } )
13	12	eleq1d	|- ( n = N -> ( { K , n } e. E <-> { K , N } e. E ) )
14	13	elrab	|- ( N e. { n e. ( Vtx ` G ) | { K , n } e. E } <-> ( N e. ( Vtx ` G ) /\ { K , N } e. E ) )
15	14	a1i	|- ( G e. USGraph -> ( N e. { n e. ( Vtx ` G ) | { K , n } e. E } <-> ( N e. ( Vtx ` G ) /\ { K , N } e. E ) ) )
16	8 11 15	3bitr4rd	|- ( G e. USGraph -> ( N e. { n e. ( Vtx ` G ) | { K , n } e. E } <-> { N , K } e. E ) )
17	4 16	bitrd	|- ( G e. USGraph -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. E ) )