MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fusgrusgr Structured version   Visualization version   GIF version

Theorem fusgrusgr 27115
Description: A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020.) (Revised by AV, 21-Oct-2020.)
Assertion
Ref Expression
fusgrusgr (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)

Proof of Theorem fusgrusgr
StepHypRef Expression
1 eqid 2801 . . 3 (Vtx‘𝐺) = (Vtx‘𝐺)
21isfusgr 27111 . 2 (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ (Vtx‘𝐺) ∈ Fin))
32simplbi 501 1 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cfv 6328  Fincfn 8496  Vtxcvtx 26792  USGraphcusgr 26945  FinUSGraphcfusgr 27109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-fusgr 27110
This theorem is referenced by:  fusgredgfi  27118  fusgrfisstep  27122  fusgrfupgrfs  27124  nbfiusgrfi  27168  vtxdgfusgrf  27290  usgruvtxvdb  27322  vdiscusgrb  27323  vdiscusgr  27324  fusgrn0eqdrusgr  27363  wlksnfi  27696  fusgrhashclwwlkn  27867  clwlksndivn  27874  fusgr2wsp2nb  28122  fusgreghash2wspv  28123  numclwwlk4  28174
  Copyright terms: Public domain W3C validator