Theorem fusgrusgr 29298

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

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6481  Fincfn 8869  Vtxcvtx 28972  USGraphcusgr 29125  FinUSGraphcfusgr 29292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-fusgr 29293

This theorem is referenced by:  fusgredgfi  29301  fusgrfisstep  29305  fusgrfupgrfs  29307  nbfiusgrfi  29351  vtxdgfusgrf  29474  usgruvtxvdb  29506  vdiscusgrb  29507  vdiscusgr  29508  fusgrn0eqdrusgr  29547  wlksnfi  29883  fusgrhashclwwlkn  30054  clwlksndivn  30061  fusgr2wsp2nb  30309  fusgreghash2wspv  30310  numclwwlk4  30361  clnbfiusgrfi  47874