Metamath Proof Explorer


Theorem uspgredg2vtxeu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 6-Dec-2020)

Ref Expression
Assertion uspgredg2vtxeu GUSHGraphEEdgGYE∃!yVtxGE=Yy

Proof

Step Hyp Ref Expression
1 uspgrupgr GUSHGraphGUPGraph
2 eqid VtxG=VtxG
3 eqid EdgG=EdgG
4 2 3 upgredg2vtx GUPGraphEEdgGYEyVtxGE=Yy
5 1 4 syl3an1 GUSHGraphEEdgGYEyVtxGE=Yy
6 eqtr2 E=YyE=YxYy=Yx
7 vex yV
8 vex xV
9 7 8 preqr2 Yy=Yxy=x
10 6 9 syl E=YyE=Yxy=x
11 10 a1i GUSHGraphEEdgGYEyVtxGxVtxGE=YyE=Yxy=x
12 11 ralrimivva GUSHGraphEEdgGYEyVtxGxVtxGE=YyE=Yxy=x
13 preq2 y=xYy=Yx
14 13 eqeq2d y=xE=YyE=Yx
15 14 reu4 ∃!yVtxGE=YyyVtxGE=YyyVtxGxVtxGE=YyE=Yxy=x
16 5 12 15 sylanbrc GUSHGraphEEdgGYE∃!yVtxGE=Yy