Theorem edgval 29122

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 6834	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5887	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29121	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6847	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7852	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6941	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5875	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6826	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5887	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6826	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2782	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 182	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  ran crn 5625  ‘cfv 6492  iEdgciedg 29070  Edgcedg 29120

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-edg 29121

This theorem is referenced by:  iedgedg  29123  edgopval  29124  edgstruct  29126  edgiedgb  29127  edg0iedg0  29128  uhgredgn0  29201  upgredgss  29205  umgredgss  29206  edgupgr  29207  uhgrvtxedgiedgb  29209  upgredg  29210  usgredgss  29232  ausgrumgri  29240  ausgrusgri  29241  uspgrf1oedg  29246  uspgrupgrushgr  29252  usgrumgruspgr  29255  usgruspgrb  29256  usgrf1oedg  29280  uhgr2edg  29281  usgrsizedg  29288  usgredg3  29289  ushgredgedg  29302  ushgredgedgloop  29304  usgr1e  29318  edg0usgr  29326  usgr1v0edg  29330  usgrexmpledg  29335  subgrprop3  29349  0grsubgr  29351  0uhgrsubgr  29352  subgruhgredgd  29357  uhgrspansubgrlem  29363  uhgrspan1  29376  upgrres1  29386  usgredgffibi  29397  dfnbgr3  29411  nbupgrres  29437  usgrnbcnvfv  29438  cplgrop  29510  cusgrexi  29516  structtocusgr  29519  cusgrsize  29528  1loopgredg  29575  1egrvtxdg0  29585  umgr2v2eedg  29598  edginwlk  29708  wlkl1loop  29711  wlkvtxedg  29717  uspgr2wlkeq  29719  wlkiswwlks1  29940  wlkiswwlks2lem4  29945  wlkiswwlks2lem5  29946  wlkiswwlks2  29948  wlkiswwlksupgr2  29950  2pthon3v  30016  usgrwwlks2on  30031  umgrwwlks2on  30032  clwlkclwwlk  30077  lfuhgr  35312  loop1cycl  35331  dfclnbgr3  48068  isubgredgss  48107  isubgredg  48108  isuspgrim0lem  48135  upgrimtrlslem2  48147  gricushgr  48159  ushggricedg  48169  stgredg  48198  usgrexmpl1edg  48266  usgrexmpl2edg  48271  gpgedg  48287