Theorem edgval 28983

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 6861	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5905	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 28982	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6874	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7889	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6971	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5892	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6853	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5905	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6853	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2776	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 182	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ∅c0 4299  ran crn 5642  ‘cfv 6514  iEdgciedg 28931  Edgcedg 28981

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-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  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-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-edg 28982

This theorem is referenced by:  iedgedg  28984  edgopval  28985  edgstruct  28987  edgiedgb  28988  edg0iedg0  28989  uhgredgn0  29062  upgredgss  29066  umgredgss  29067  edgupgr  29068  uhgrvtxedgiedgb  29070  upgredg  29071  usgredgss  29093  ausgrumgri  29101  ausgrusgri  29102  uspgrf1oedg  29107  uspgrupgrushgr  29113  usgrumgruspgr  29116  usgruspgrb  29117  usgrf1oedg  29141  uhgr2edg  29142  usgrsizedg  29149  usgredg3  29150  ushgredgedg  29163  ushgredgedgloop  29165  usgr1e  29179  edg0usgr  29187  usgr1v0edg  29191  usgrexmpledg  29196  subgrprop3  29210  0grsubgr  29212  0uhgrsubgr  29213  subgruhgredgd  29218  uhgrspansubgrlem  29224  uhgrspan1  29237  upgrres1  29247  usgredgffibi  29258  dfnbgr3  29272  nbupgrres  29298  usgrnbcnvfv  29299  cplgrop  29371  cusgrexi  29377  structtocusgr  29380  cusgrsize  29389  1loopgredg  29436  1egrvtxdg0  29446  umgr2v2eedg  29459  edginwlk  29570  wlkl1loop  29573  wlkvtxedg  29579  uspgr2wlkeq  29581  wlkiswwlks1  29804  wlkiswwlks2lem4  29809  wlkiswwlks2lem5  29810  wlkiswwlks2  29812  wlkiswwlksupgr2  29814  2pthon3v  29880  umgrwwlks2on  29894  clwlkclwwlk  29938  lfuhgr  35112  loop1cycl  35131  dfclnbgr3  47831  isubgredgss  47869  isubgredg  47870  isuspgrim0lem  47897  upgrimtrlslem2  47909  gricushgr  47921  ushggricedg  47931  stgredg  47959  usgrexmpl1edg  48019  usgrexmpl2edg  48024  gpgedg  48040