Metamath Proof Explorer

Theorem usgredgppr

Description: An edge of a simple graph is a proper pair, i.e. a set containing two different elements (the endvertices of the edge). Analogue of usgredg2 . (Contributed by Alexander van der Vekens, 11-Aug-2017) (Revised by AV, 9-Jan-2020) (Revised by AV, 23-Oct-2020)

Ref Expression
Hypothesis usgredgppr.e ⊢ E = Edg ⁡ G
Assertion usgredgppr ⊢ G ∈ USGraph ∧ C ∈ E → C = 2

Proof

Step Hyp Ref Expression
1 usgredgppr.e ⊢ E = Edg ⁡ G
2 1 eleq2i ⊢ C ∈ E ↔ C ∈ Edg ⁡ G
3 edgusgr ⊢ G ∈ USGraph ∧ C ∈ Edg ⁡ G → C ∈ 𝒫 Vtx ⁡ G ∧ C = 2
4 2 3 sylan2b ⊢ G ∈ USGraph ∧ C ∈ E → C ∈ 𝒫 Vtx ⁡ G ∧ C = 2
5 4 simprd ⊢ G ∈ USGraph ∧ C ∈ E → C = 2