Metamath Proof Explorer

Theorem edgssv2

Description: An edge of a simple graph is an unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020) (Revised by AV, 23-Oct-2020)

Ref Expression
Hypotheses edgssv2.v ⊢V=Vtx⁡G
edgssv2.e ⊢E=Edg⁡G
Assertion edgssv2 ⊢G∈USGraph∧C∈E→C⊆V∧C=2

Proof

Step Hyp Ref Expression
1 edgssv2.v ⊢V=Vtx⁡G
2 edgssv2.e ⊢E=Edg⁡G
3 2 eleq2i ⊢C∈E↔C∈Edg⁡G
4 edgusgr ⊢G∈USGraph∧C∈Edg⁡G→C∈𝒫Vtx⁡G∧C=2
5 3 4 sylan2b ⊢G∈USGraph∧C∈E→C∈𝒫Vtx⁡G∧C=2
6 elpwi ⊢C∈𝒫Vtx⁡G→C⊆Vtx⁡G
7 6 anim1i ⊢C∈𝒫Vtx⁡G∧C=2→C⊆Vtx⁡G∧C=2
8 5 7 syl ⊢G∈USGraph∧C∈E→C⊆Vtx⁡G∧C=2
9 1 a1i ⊢G∈USGraph∧C∈E→V=Vtx⁡G
10 9 sseq2d ⊢G∈USGraph∧C∈E→C⊆V↔C⊆Vtx⁡G
11 10 anbi1d ⊢G∈USGraph∧C∈E→C⊆V∧C=2↔C⊆Vtx⁡G∧C=2
12 8 11 mpbird ⊢G∈USGraph∧C∈E→C⊆V∧C=2