Theorem edgval 29012

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 6826	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5884	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29011	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6839	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7850	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6934	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5872	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6818	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5884	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6818	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2775	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 182	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  Vcvv 3438  ∅c0 4286  ran crn 5624  ‘cfv 6486  iEdgciedg 28960  Edgcedg 29010

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6442  df-fun 6488  df-fv 6494  df-edg 29011

This theorem is referenced by:  iedgedg  29013  edgopval  29014  edgstruct  29016  edgiedgb  29017  edg0iedg0  29018  uhgredgn0  29091  upgredgss  29095  umgredgss  29096  edgupgr  29097  uhgrvtxedgiedgb  29099  upgredg  29100  usgredgss  29122  ausgrumgri  29130  ausgrusgri  29131  uspgrf1oedg  29136  uspgrupgrushgr  29142  usgrumgruspgr  29145  usgruspgrb  29146  usgrf1oedg  29170  uhgr2edg  29171  usgrsizedg  29178  usgredg3  29179  ushgredgedg  29192  ushgredgedgloop  29194  usgr1e  29208  edg0usgr  29216  usgr1v0edg  29220  usgrexmpledg  29225  subgrprop3  29239  0grsubgr  29241  0uhgrsubgr  29242  subgruhgredgd  29247  uhgrspansubgrlem  29253  uhgrspan1  29266  upgrres1  29276  usgredgffibi  29287  dfnbgr3  29301  nbupgrres  29327  usgrnbcnvfv  29328  cplgrop  29400  cusgrexi  29406  structtocusgr  29409  cusgrsize  29418  1loopgredg  29465  1egrvtxdg0  29475  umgr2v2eedg  29488  edginwlk  29598  wlkl1loop  29601  wlkvtxedg  29607  uspgr2wlkeq  29609  wlkiswwlks1  29830  wlkiswwlks2lem4  29835  wlkiswwlks2lem5  29836  wlkiswwlks2  29838  wlkiswwlksupgr2  29840  2pthon3v  29906  umgrwwlks2on  29920  clwlkclwwlk  29964  lfuhgr  35090  loop1cycl  35109  dfclnbgr3  47811  isubgredgss  47850  isubgredg  47851  isuspgrim0lem  47878  upgrimtrlslem2  47890  gricushgr  47902  ushggricedg  47912  stgredg  47941  usgrexmpl1edg  48009  usgrexmpl2edg  48014  gpgedg  48030