Theorem edgval 29028

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 6876	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5918	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29027	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6889	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7906	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6986	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5905	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6868	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5918	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6868	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2781	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 182	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108  Vcvv 3459  ∅c0 4308  ran crn 5655  ‘cfv 6531  iEdgciedg 28976  Edgcedg 29026

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

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-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6484  df-fun 6533  df-fv 6539  df-edg 29027

This theorem is referenced by:  iedgedg  29029  edgopval  29030  edgstruct  29032  edgiedgb  29033  edg0iedg0  29034  uhgredgn0  29107  upgredgss  29111  umgredgss  29112  edgupgr  29113  uhgrvtxedgiedgb  29115  upgredg  29116  usgredgss  29138  ausgrumgri  29146  ausgrusgri  29147  uspgrf1oedg  29152  uspgrupgrushgr  29158  usgrumgruspgr  29161  usgruspgrb  29162  usgrf1oedg  29186  uhgr2edg  29187  usgrsizedg  29194  usgredg3  29195  ushgredgedg  29208  ushgredgedgloop  29210  usgr1e  29224  edg0usgr  29232  usgr1v0edg  29236  usgrexmpledg  29241  subgrprop3  29255  0grsubgr  29257  0uhgrsubgr  29258  subgruhgredgd  29263  uhgrspansubgrlem  29269  uhgrspan1  29282  upgrres1  29292  usgredgffibi  29303  dfnbgr3  29317  nbupgrres  29343  usgrnbcnvfv  29344  cplgrop  29416  cusgrexi  29422  structtocusgr  29425  cusgrsize  29434  1loopgredg  29481  1egrvtxdg0  29491  umgr2v2eedg  29504  edginwlk  29615  wlkl1loop  29618  wlkvtxedg  29624  uspgr2wlkeq  29626  wlkiswwlks1  29849  wlkiswwlks2lem4  29854  wlkiswwlks2lem5  29855  wlkiswwlks2  29857  wlkiswwlksupgr2  29859  2pthon3v  29925  umgrwwlks2on  29939  clwlkclwwlk  29983  lfuhgr  35140  loop1cycl  35159  dfclnbgr3  47840  isubgredgss  47878  isubgredg  47879  isuspgrim0lem  47906  upgrimtrlslem2  47918  gricushgr  47930  ushggricedg  47940  stgredg  47968  usgrexmpl1edg  48028  usgrexmpl2edg  48033  gpgedg  48049