Theorem edgval 29025

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 6822	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5878	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29024	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6835	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7840	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6929	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5866	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6814	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5878	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6814	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2777	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 182	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ∅c0 4283  ran crn 5617  ‘cfv 6481  iEdgciedg 28973  Edgcedg 29023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-iota 6437  df-fun 6483  df-fv 6489  df-edg 29024

This theorem is referenced by:  iedgedg  29026  edgopval  29027  edgstruct  29029  edgiedgb  29030  edg0iedg0  29031  uhgredgn0  29104  upgredgss  29108  umgredgss  29109  edgupgr  29110  uhgrvtxedgiedgb  29112  upgredg  29113  usgredgss  29135  ausgrumgri  29143  ausgrusgri  29144  uspgrf1oedg  29149  uspgrupgrushgr  29155  usgrumgruspgr  29158  usgruspgrb  29159  usgrf1oedg  29183  uhgr2edg  29184  usgrsizedg  29191  usgredg3  29192  ushgredgedg  29205  ushgredgedgloop  29207  usgr1e  29221  edg0usgr  29229  usgr1v0edg  29233  usgrexmpledg  29238  subgrprop3  29252  0grsubgr  29254  0uhgrsubgr  29255  subgruhgredgd  29260  uhgrspansubgrlem  29266  uhgrspan1  29279  upgrres1  29289  usgredgffibi  29300  dfnbgr3  29314  nbupgrres  29340  usgrnbcnvfv  29341  cplgrop  29413  cusgrexi  29419  structtocusgr  29422  cusgrsize  29431  1loopgredg  29478  1egrvtxdg0  29488  umgr2v2eedg  29501  edginwlk  29611  wlkl1loop  29614  wlkvtxedg  29620  uspgr2wlkeq  29622  wlkiswwlks1  29843  wlkiswwlks2lem4  29848  wlkiswwlks2lem5  29849  wlkiswwlks2  29851  wlkiswwlksupgr2  29853  2pthon3v  29919  umgrwwlks2on  29933  clwlkclwwlk  29977  lfuhgr  35150  loop1cycl  35169  dfclnbgr3  47856  isubgredgss  47895  isubgredg  47896  isuspgrim0lem  47923  upgrimtrlslem2  47935  gricushgr  47947  ushggricedg  47957  stgredg  47986  usgrexmpl1edg  48054  usgrexmpl2edg  48059  gpgedg  48075