Theorem usgredgreu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

	Ref	Expression
Hypotheses	usgredg3.v	|- V = ( Vtx ` G )
	usgredg3.e	|- E = ( iEdg ` G )
Assertion	usgredgreu	|- ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E! y e. V ( E ` X ) = { Y , y } )

Proof

Step	Hyp	Ref	Expression
1		usgredg3.v	|- V = ( Vtx ` G )
2		usgredg3.e	|- E = ( iEdg ` G )
3	1 2	usgredg4	|- ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E. y e. V ( E ` X ) = { Y , y } )
4		eqtr2	|- ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> { Y , y } = { Y , x } )
5		vex	|- y e. _V
6		vex	|- x e. _V
7	5 6	preqr2	|- ( { Y , y } = { Y , x } -> y = x )
8	4 7	syl	|- ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> y = x )
9	8	a1i	|- ( ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) /\ ( y e. V /\ x e. V ) ) -> ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> y = x ) )
10	9	ralrimivva	|- ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> A. y e. V A. x e. V ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> y = x ) )
11		preq2	|- ( y = x -> { Y , y } = { Y , x } )
12	11	eqeq2d	|- ( y = x -> ( ( E ` X ) = { Y , y } <-> ( E ` X ) = { Y , x } ) )
13	12	reu4	|- ( E! y e. V ( E ` X ) = { Y , y } <-> ( E. y e. V ( E ` X ) = { Y , y } /\ A. y e. V A. x e. V ( ( ( E ` X ) = { Y , y } /\ ( E ` X ) = { Y , x } ) -> y = x ) ) )
14	3 10 13	sylanbrc	|- ( ( G e. USGraph /\ X e. dom E /\ Y e. ( E ` X ) ) -> E! y e. V ( E ` X ) = { Y , y } )