{
  "citations" : [ {
    "textCitation" : "[See usgrafiedg on Metamath](http://us.metamath.org/mpegif/usgrafiedg.html)"
  } ],
  "names" : [ "usgrafiedg" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_cG", "#T_wcel", "#T_cusg", "#T_wa", "#T_c1st", "#T_cfv", "#T_cG", "#T_wcel", "#T_cfn", "#T_wi", "#T_cedg", "#T_cfv", "#T_cG", "#T_wcel", "#T_cfn" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " A simple undirected graph with a finite number of vertices has also only a finite number of edges.  (Contributed by AV, 2-Jan-2020.) ",
  "statement" : "usgrafiedg $p |- ( ( G e. USGrph /\\ ( 1st ` G ) e. Fin ) -> ( Edges ` G ) e. Fin ) $."
}