Theorem nbusgrf1o

Description: The set of neighbors of a vertex is isomorphic to the set of edges containing the vertex in a simple graph. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 28-Oct-2020)

	Ref	Expression
Hypotheses	nbusgrf1o.v	|- V = ( Vtx ` G )
	nbusgrf1o.e	|- E = ( Edg ` G )
Assertion	nbusgrf1o	|- ( ( G e. USGraph /\ U e. V ) -> E. f f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } )

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o.v	|- V = ( Vtx ` G )
2		nbusgrf1o.e	|- E = ( Edg ` G )
3		eqid	|- ( G NeighbVtx U ) = ( G NeighbVtx U )
4		eleq2w	|- ( e = c -> ( U e. e <-> U e. c ) )
5	4	cbvrabv	|- { e e. E | U e. e } = { c e. E | U e. c }
6	1 2 3 5	nbusgrf1o1	|- ( ( G e. USGraph /\ U e. V ) -> E. f f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } )