Theorem edgval 29609

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 6877	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5920	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29608	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6890	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7911	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6985	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5908	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6869	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5920	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6869	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2807	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 184	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  Vcvv 3451  ∅c0 4279  ran crn 5652  ‘cfv 6531  iEdgciedg 29557  Edgcedg 29607

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fv 6539  df-edg 29608

This theorem is used by:  iedgedg  29610  edgopval  29611  edgstruct  29613  edgiedgb  29614  edg0iedg0  29615  uhgredgn0  29688  upgredgss  29692  umgredgss  29693  edgupgr  29694  uhgrvtxedgiedgb  29696  upgredg  29697  lfuhgr  29708  usgredgss  29722  ausgrumgri  29730  ausgrusgri  29731  uspgrf1oedg  29736  uspgrupgrushgr  29742  usgrumgruspgr  29745  usgruspgrb  29746  usgrf1oedg  29770  uhgr2edg  29771  usgrsizedg  29778  usgredg3  29779  ushgredgedg  29792  ushgredgedgloop  29794  usgr1e  29808  edg0usgr  29816  usgr1v0edg  29820  usgrexmpledg  29825  subgrprop3  29839  0grsubgr  29841  0uhgrsubgr  29842  subgruhgredgd  29847  uhgrspansubgrlem  29853  uhgrspan1  29866  upgrres1  29876  usgredgffibi  29887  dfnbgr3  29901  nbupgrres  29927  usgrnbcnvfv  29928  cplgrop  30000  cusgrexi  30006  structtocusgr  30009  cusgrsize  30017  1loopgredg  30064  1egrvtxdg0  30074  umgr2v2eedg  30087  edginwlk  30197  wlkl1loop  30200  wlkvtxedg  30206  uspgr2wlkeq  30208  wlkiswwlks1  30438  wlkiswwlks2lem4  30443  wlkiswwlks2lem5  30444  wlkiswwlks2  30446  wlkiswwlksupgr2  30448  2pthon3v  30514  usgrwwlks2on  30529  umgrwwlks2on  30530  clwlkclwwlk  30575  loop1cycl  30726  dfclnbgr3  48868  isubgredgss  48907  isubgredg  48908  isuspgrim0lem  48935  upgrimtrlslem2  48947  gricushgr  48959  ushggricedg  48969  stgredg  48998  usgrexmpl1edg  49066  usgrexmpl2edg  49071  gpgedg  49087