Theorem edgval 29196

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 6863	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5912	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29195	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6876	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7887	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6971	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5900	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6855	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5912	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6855	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2807	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 183	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1559   ∈ wcel 2141  Vcvv 3453  ∅c0 4285  ran crn 5646  ‘cfv 6517  iEdgciedg 29144  Edgcedg 29194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fv 6525  df-edg 29195

This theorem is referenced by:  iedgedg  29197  edgopval  29198  edgstruct  29200  edgiedgb  29201  edg0iedg0  29202  uhgredgn0  29275  upgredgss  29279  umgredgss  29280  edgupgr  29281  uhgrvtxedgiedgb  29283  upgredg  29284  usgredgss  29306  ausgrumgri  29314  ausgrusgri  29315  uspgrf1oedg  29320  uspgrupgrushgr  29326  usgrumgruspgr  29329  usgruspgrb  29330  usgrf1oedg  29354  uhgr2edg  29355  usgrsizedg  29362  usgredg3  29363  ushgredgedg  29376  ushgredgedgloop  29378  usgr1e  29392  edg0usgr  29400  usgr1v0edg  29404  usgrexmpledg  29409  subgrprop3  29423  0grsubgr  29425  0uhgrsubgr  29426  subgruhgredgd  29431  uhgrspansubgrlem  29437  uhgrspan1  29450  upgrres1  29460  usgredgffibi  29471  dfnbgr3  29485  nbupgrres  29511  usgrnbcnvfv  29512  cplgrop  29584  cusgrexi  29590  structtocusgr  29593  cusgrsize  29601  1loopgredg  29648  1egrvtxdg0  29658  umgr2v2eedg  29671  edginwlk  29781  wlkl1loop  29784  wlkvtxedg  29790  uspgr2wlkeq  29792  wlkiswwlks1  30013  wlkiswwlks2lem4  30018  wlkiswwlks2lem5  30019  wlkiswwlks2  30021  wlkiswwlksupgr2  30023  2pthon3v  30089  usgrwwlks2on  30104  umgrwwlks2on  30105  clwlkclwwlk  30150  lfuhgr  35432  loop1cycl  35451  dfclnbgr3  48412  isubgredgss  48451  isubgredg  48452  isuspgrim0lem  48479  upgrimtrlslem2  48491  gricushgr  48503  ushggricedg  48513  stgredg  48542  usgrexmpl1edg  48610  usgrexmpl2edg  48615  gpgedg  48631