Theorem edgval 29308

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 6871	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5919	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29307	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6884	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7895	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6979	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5907	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6863	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5919	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6863	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2811	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 184	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1563   ∈ wcel 2145  Vcvv 3457  ∅c0 4288  ran crn 5653  ‘cfv 6525  iEdgciedg 29256  Edgcedg 29306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fv 6533  df-edg 29307

This theorem is referenced by:  iedgedg  29309  edgopval  29310  edgstruct  29312  edgiedgb  29313  edg0iedg0  29314  uhgredgn0  29387  upgredgss  29391  umgredgss  29392  edgupgr  29393  uhgrvtxedgiedgb  29395  upgredg  29396  usgredgss  29418  ausgrumgri  29426  ausgrusgri  29427  uspgrf1oedg  29432  uspgrupgrushgr  29438  usgrumgruspgr  29441  usgruspgrb  29442  usgrf1oedg  29466  uhgr2edg  29467  usgrsizedg  29474  usgredg3  29475  ushgredgedg  29488  ushgredgedgloop  29490  usgr1e  29504  edg0usgr  29512  usgr1v0edg  29516  usgrexmpledg  29521  subgrprop3  29535  0grsubgr  29537  0uhgrsubgr  29538  subgruhgredgd  29543  uhgrspansubgrlem  29549  uhgrspan1  29562  upgrres1  29572  usgredgffibi  29583  dfnbgr3  29597  nbupgrres  29623  usgrnbcnvfv  29624  cplgrop  29696  cusgrexi  29702  structtocusgr  29705  cusgrsize  29713  1loopgredg  29760  1egrvtxdg0  29770  umgr2v2eedg  29783  edginwlk  29893  wlkl1loop  29896  wlkvtxedg  29902  uspgr2wlkeq  29904  wlkiswwlks1  30125  wlkiswwlks2lem4  30130  wlkiswwlks2lem5  30131  wlkiswwlks2  30133  wlkiswwlksupgr2  30135  2pthon3v  30201  usgrwwlks2on  30216  umgrwwlks2on  30217  clwlkclwwlk  30262  lfuhgr  35481  loop1cycl  35500  dfclnbgr3  48446  isubgredgss  48485  isubgredg  48486  isuspgrim0lem  48513  upgrimtrlslem2  48525  gricushgr  48537  ushggricedg  48547  stgredg  48576  usgrexmpl1edg  48644  usgrexmpl2edg  48649  gpgedg  48665