Metamath Proof Explorer

Theorem edgusgr

Description: An edge of a simple graph is a proper 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