Theorem fusgrusgr 29885

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6531  Fincfn 8957  Vtxcvtx 29556  USGraphcusgr 29712  FinUSGraphcfusgr 29879

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-fusgr 29880

This theorem is used by:  fusgredgfi  29888  fusgrfisstep  29892  fusgrfupgrfs  29894  nbfiusgrfi  29938  vtxdgfusgrf  30060  usgruvtxvdb  30092  vdiscusgrb  30093  vdiscusgr  30094  fusgrn0eqdrusgr  30133  wlksnfi  30478  fusgrhashclwwlkn  30652  clwlksndivn  30659  fusgr2wsp2nb  30917  fusgreghash2wspv  30918  numclwwlk4  30969  clnbfiusgrfi  48886