Metamath Proof Explorer


Theorem usgrf

Description: The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 13-Oct-2020)

Ref Expression
Hypotheses isuspgr.v 𝑉 = ( Vtx ‘ 𝐺 )
isuspgr.e 𝐸 = ( iEdg ‘ 𝐺 )
Assertion usgrf ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )

Proof

Step Hyp Ref Expression
1 isuspgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 isuspgr.e 𝐸 = ( iEdg ‘ 𝐺 )
3 1 2 isusgr ( 𝐺 ∈ USGraph → ( 𝐺 ∈ USGraph ↔ 𝐸 : dom 𝐸1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
4 3 ibi ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )