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	⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2	1	isfusgr	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) )
3	2	simplbi	⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )