Metamath Proof Explorer

Theorem fusgrusgr

Description: A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020) (Revised by AV, 21-Oct-2020)

Ref Expression
Assertion fusgrusgr ⊢ G ∈ FinUSGraph → G ∈ USGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 isfusgr ⊢ G ∈ FinUSGraph ↔ G ∈ USGraph ∧ Vtx ⁡ G ∈ Fin
3 2 simplbi ⊢ G ∈ FinUSGraph → G ∈ USGraph