Theorem fusgrusgr 29909

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 2760	. . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2	1	isfusgr 29905	. 2 ⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ (Vtx‘𝐺) ∈ Fin))
3	2	simplbi 502	1 ⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ‘cfv 6539  Fincfn 8977  Vtxcvtx 29580  USGraphcusgr 29736  FinUSGraphcfusgr 29903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-fusgr 29904

This theorem is used by:  fusgredgfi  29912  fusgrfisstep  29916  fusgrfupgrfs  29918  nbfiusgrfi  29962  vtxdgfusgrf  30084  usgruvtxvdb  30116  vdiscusgrb  30117  vdiscusgr  30118  fusgrn0eqdrusgr  30157  wlksnfi  30502  fusgrhashclwwlkn  30676  clwlksndivn  30683  fusgr2wsp2nb  30941  fusgreghash2wspv  30942  numclwwlk4  30993  clnbfiusgrfi  49036