Metamath Proof Explorer

Theorem edgumgr

Description: Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020)

Ref Expression
Assertion edgumgr ⊢ G ∈ UMGraph ∧ E ∈ Edg ⁡ G → E ∈ 𝒫 Vtx ⁡ G ∧ E = 2

Proof

Step Hyp Ref Expression
1 umgredgss ⊢ G ∈ UMGraph → Edg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G | x = 2
2 1 sselda ⊢ G ∈ UMGraph ∧ 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 ∈ UMGraph ∧ E ∈ Edg ⁡ G → E ∈ 𝒫 Vtx ⁡ G ∧ E = 2