Metamath Proof Explorer

Theorem usgredgop

Description: An edge of a simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017) (Proof shortened by Alexander van der Vekens, 16-Dec-2017) (Revised by AV, 15-Oct-2020)

Ref Expression
Assertion usgredgop ⊢ G ∈ USGraph ∧ E = iEdg ⁡ G ∧ X ∈ dom ⁡ E → E ⁡ X = M N ↔ X M N ∈ E

Proof

Step Hyp Ref Expression
1 usgrfun ⊢ G ∈ USGraph → Fun ⁡ iEdg ⁡ G
2 funeq ⊢ E = iEdg ⁡ G → Fun ⁡ E ↔ Fun ⁡ iEdg ⁡ G
3 1 2 syl5ibrcom ⊢ G ∈ USGraph → E = iEdg ⁡ G → Fun ⁡ E
4 3 imp ⊢ G ∈ USGraph ∧ E = iEdg ⁡ G → Fun ⁡ E
5 funopfvb ⊢ Fun ⁡ E ∧ X ∈ dom ⁡ E → E ⁡ X = M N ↔ X M N ∈ E
6 4 5 stoic3 ⊢ G ∈ USGraph ∧ E = iEdg ⁡ G ∧ X ∈ dom ⁡ E → E ⁡ X = M N ↔ X M N ∈ E