Theorem fusgrusgr 29301

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6531  Fincfn 8959  Vtxcvtx 28975  USGraphcusgr 29128  FinUSGraphcfusgr 29295

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-fusgr 29296

This theorem is referenced by:  fusgredgfi  29304  fusgrfisstep  29308  fusgrfupgrfs  29310  nbfiusgrfi  29354  vtxdgfusgrf  29477  usgruvtxvdb  29509  vdiscusgrb  29510  vdiscusgr  29511  fusgrn0eqdrusgr  29550  wlksnfi  29889  fusgrhashclwwlkn  30060  clwlksndivn  30067  fusgr2wsp2nb  30315  fusgreghash2wspv  30316  numclwwlk4  30367  clnbfiusgrfi  47857