Theorem edgval 29657

Description: The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.)

Assertion

Ref	Expression
edgval	⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Proof of Theorem edgval

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6908	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5927	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29656	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6921	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7946	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 7016	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5915	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6900	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5927	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6900	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2809	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 184	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ∅c0 4281  ran crn 5656  ‘cfv 6558  iEdgciedg 29605  Edgcedg 29655

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

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-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fv 6566  df-edg 29656

This theorem is used by:  iedgedg  29658  edgopval  29659  edgstruct  29661  edgiedgb  29662  edg0iedg0  29663  uhgredgn0  29736  upgredgss  29740  umgredgss  29741  edgupgr  29742  uhgrvtxedgiedgb  29744  upgredg  29745  lfuhgr  29756  usgredgss  29770  ausgrumgri  29778  ausgrusgri  29779  uspgrf1oedg  29784  uspgrupgrushgr  29790  usgrumgruspgr  29793  usgruspgrb  29794  usgrf1oedg  29818  uhgr2edg  29819  usgrsizedg  29826  usgredg3  29827  ushgredgedg  29840  ushgredgedgloop  29842  usgr1e  29856  edg0usgr  29864  usgr1v0edg  29868  usgrexmpledg  29873  subgrprop3  29887  0grsubgr  29889  0uhgrsubgr  29890  subgruhgredgd  29895  uhgrspansubgrlem  29901  uhgrspan1  29914  upgrres1  29924  usgredgffibi  29935  dfnbgr3  29949  nbupgrres  29975  usgrnbcnvfv  29976  cplgrop  30048  cusgrexi  30054  structtocusgr  30057  cusgrsize  30065  1loopgredg  30112  1egrvtxdg0  30122  umgr2v2eedg  30135  edginwlk  30245  wlkl1loop  30248  wlkvtxedg  30254  uspgr2wlkeq  30256  wlkiswwlks1  30486  wlkiswwlks2lem4  30491  wlkiswwlks2lem5  30492  wlkiswwlks2  30494  wlkiswwlksupgr2  30496  2pthon3v  30562  usgrwwlks2on  30577  umgrwwlks2on  30578  clwlkclwwlk  30623  loop1cycl  30774  dfclnbgr3  49129  isubgredgss  49168  isubgredg  49169  isuspgrim0lem  49196  upgrimtrlslem2  49208  gricushgr  49220  ushggricedg  49230  stgredg  49259  usgrexmpl1edg  49327  usgrexmpl2edg  49332  gpgedg  49348