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

Theorem fusgrusgr 28846
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 2730 . . 3 (Vtx‘𝐺) = (Vtx‘𝐺)
21isfusgr 28842 . 2 (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ (Vtx‘𝐺) ∈ Fin))
32simplbi 496 1 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ∈ wcel 2104  â€˜cfv 6542  Fincfn 8941  Vtxcvtx 28523  USGraphcusgr 28676  FinUSGraphcfusgr 28840
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-fusgr 28841
This theorem is referenced by:  fusgredgfi  28849  fusgrfisstep  28853  fusgrfupgrfs  28855  nbfiusgrfi  28899  vtxdgfusgrf  29021  usgruvtxvdb  29053  vdiscusgrb  29054  vdiscusgr  29055  fusgrn0eqdrusgr  29094  wlksnfi  29428  fusgrhashclwwlkn  29599  clwlksndivn  29606  fusgr2wsp2nb  29854  fusgreghash2wspv  29855  numclwwlk4  29906
  Copyright terms: Public domain W3C validator