Metamath Proof Explorer

Theorem edgusgr

Description: An edge of a simple graph is an unordered pair of vertices. (Contributed by AV, 1-Jan-2020) (Revised by AV, 14-Oct-2020)

Ref Expression
Assertion edgusgr ⊢G∈USGraph∧E∈Edg⁡G→E∈𝒫Vtx⁡G∧E=2

Proof

Step Hyp Ref Expression
1 usgredgss ⊢G∈USGraph→Edg⁡G⊆x∈𝒫Vtx⁡G|x=2
2 1 sselda ⊢G∈USGraph∧E∈Edg⁡G→E∈x∈𝒫Vtx⁡G|x=2
3 fveqeq2 ⊢x=E→x=2↔E=2
4 3 elrab ⊢E∈x∈𝒫Vtx⁡G|x=2↔E∈𝒫Vtx⁡G∧E=2
5 2 4 sylib ⊢G∈USGraph∧E∈Edg⁡G→E∈𝒫Vtx⁡G∧E=2