Theorem edgval 29143

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 29142	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6847	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7857	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6942	. 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 2786	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 183	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1547   ∈ wcel 2119  Vcvv 3432  ∅c0 4268  ran crn 5626  ‘cfv 6492  iEdgciedg 29091  Edgcedg 29141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fv 6500  df-edg 29142

This theorem is referenced by:  iedgedg  29144  edgopval  29145  edgstruct  29147  edgiedgb  29148  edg0iedg0  29149  uhgredgn0  29222  upgredgss  29226  umgredgss  29227  edgupgr  29228  uhgrvtxedgiedgb  29230  upgredg  29231  usgredgss  29253  ausgrumgri  29261  ausgrusgri  29262  uspgrf1oedg  29267  uspgrupgrushgr  29273  usgrumgruspgr  29276  usgruspgrb  29277  usgrf1oedg  29301  uhgr2edg  29302  usgrsizedg  29309  usgredg3  29310  ushgredgedg  29323  ushgredgedgloop  29325  usgr1e  29339  edg0usgr  29347  usgr1v0edg  29351  usgrexmpledg  29356  subgrprop3  29370  0grsubgr  29372  0uhgrsubgr  29373  subgruhgredgd  29378  uhgrspansubgrlem  29384  uhgrspan1  29397  upgrres1  29407  usgredgffibi  29418  dfnbgr3  29432  nbupgrres  29458  usgrnbcnvfv  29459  cplgrop  29531  cusgrexi  29537  structtocusgr  29540  cusgrsize  29548  1loopgredg  29595  1egrvtxdg0  29605  umgr2v2eedg  29618  edginwlk  29728  wlkl1loop  29731  wlkvtxedg  29737  uspgr2wlkeq  29739  wlkiswwlks1  29960  wlkiswwlks2lem4  29965  wlkiswwlks2lem5  29966  wlkiswwlks2  29968  wlkiswwlksupgr2  29970  2pthon3v  30036  usgrwwlks2on  30051  umgrwwlks2on  30052  clwlkclwwlk  30097  lfuhgr  35353  loop1cycl  35372  dfclnbgr3  48324  isubgredgss  48363  isubgredg  48364  isuspgrim0lem  48391  upgrimtrlslem2  48403  gricushgr  48415  ushggricedg  48425  stgredg  48454  usgrexmpl1edg  48522  usgrexmpl2edg  48527  gpgedg  48543