Theorem upgredg2vtx

Description: For a vertex incident to an edge there is another vertex incident to the edge in a pseudograph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 5-Dec-2020)

	Ref	Expression
Hypotheses	upgredg.v	|- V = ( Vtx ` G )
	upgredg.e	|- E = ( Edg ` G )
Assertion	upgredg2vtx	|- ( ( G e. UPGraph /\ C e. E /\ A e. C ) -> E. b e. V C = { A , b } )

Proof

Step	Hyp	Ref	Expression
1		upgredg.v	|- V = ( Vtx ` G )
2		upgredg.e	|- E = ( Edg ` G )
3	1 2	upgredg	|- ( ( G e. UPGraph /\ C e. E ) -> E. a e. V E. c e. V C = { a , c } )
4	3	3adant3	|- ( ( G e. UPGraph /\ C e. E /\ A e. C ) -> E. a e. V E. c e. V C = { a , c } )
5		elpr2elpr	|- ( ( a e. V /\ c e. V /\ A e. { a , c } ) -> E. b e. V { a , c } = { A , b } )
6	5	3expia	|- ( ( a e. V /\ c e. V ) -> ( A e. { a , c } -> E. b e. V { a , c } = { A , b } ) )
7		eleq2	|- ( C = { a , c } -> ( A e. C <-> A e. { a , c } ) )
8		eqeq1	|- ( C = { a , c } -> ( C = { A , b } <-> { a , c } = { A , b } ) )
9	8	rexbidv	|- ( C = { a , c } -> ( E. b e. V C = { A , b } <-> E. b e. V { a , c } = { A , b } ) )
10	7 9	imbi12d	|- ( C = { a , c } -> ( ( A e. C -> E. b e. V C = { A , b } ) <-> ( A e. { a , c } -> E. b e. V { a , c } = { A , b } ) ) )
11	6 10	imbitrrid	|- ( C = { a , c } -> ( ( a e. V /\ c e. V ) -> ( A e. C -> E. b e. V C = { A , b } ) ) )
12	11	com13	|- ( A e. C -> ( ( a e. V /\ c e. V ) -> ( C = { a , c } -> E. b e. V C = { A , b } ) ) )
13	12	3ad2ant3	|- ( ( G e. UPGraph /\ C e. E /\ A e. C ) -> ( ( a e. V /\ c e. V ) -> ( C = { a , c } -> E. b e. V C = { A , b } ) ) )
14	13	rexlimdvv	|- ( ( G e. UPGraph /\ C e. E /\ A e. C ) -> ( E. a e. V E. c e. V C = { a , c } -> E. b e. V C = { A , b } ) )
15	4 14	mpd	|- ( ( G e. UPGraph /\ C e. E /\ A e. C ) -> E. b e. V C = { A , b } )