Theorem fusgrusgr 29256

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6514  Fincfn 8921  Vtxcvtx 28930  USGraphcusgr 29083  FinUSGraphcfusgr 29250

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-fusgr 29251

This theorem is referenced by:  fusgredgfi  29259  fusgrfisstep  29263  fusgrfupgrfs  29265  nbfiusgrfi  29309  vtxdgfusgrf  29432  usgruvtxvdb  29464  vdiscusgrb  29465  vdiscusgr  29466  fusgrn0eqdrusgr  29505  wlksnfi  29844  fusgrhashclwwlkn  30015  clwlksndivn  30022  fusgr2wsp2nb  30270  fusgreghash2wspv  30271  numclwwlk4  30322  clnbfiusgrfi  47848