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 e. FinUSGraph -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ ( Vtx ` G ) e. Fin ) )
3 2 simplbi 
 |-  ( G e. FinUSGraph -> G e. USGraph )