Theorem fusgrusgr 29416

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

Syntax hints:   → wi 4   ∈ wcel 2119  ‘cfv 6492  Fincfn 8890  Vtxcvtx 29090  USGraphcusgr 29243  FinUSGraphcfusgr 29410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-fusgr 29411

This theorem is referenced by:  fusgredgfi  29419  fusgrfisstep  29423  fusgrfupgrfs  29425  nbfiusgrfi  29469  vtxdgfusgrf  29591  usgruvtxvdb  29623  vdiscusgrb  29624  vdiscusgr  29625  fusgrn0eqdrusgr  29664  wlksnfi  30000  fusgrhashclwwlkn  30174  clwlksndivn  30181  fusgr2wsp2nb  30429  fusgreghash2wspv  30430  numclwwlk4  30481  clnbfiusgrfi  48342