Theorem edgval 29514

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 6882	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5926	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29513	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6895	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7911	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6990	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5914	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6874	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5926	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6874	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2808	. 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 3453  ∅c0 4282  ran crn 5660  ‘cfv 6537  iEdgciedg 29462  Edgcedg 29512

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fv 6545  df-edg 29513

This theorem is used by:  iedgedg  29515  edgopval  29516  edgstruct  29518  edgiedgb  29519  edg0iedg0  29520  uhgredgn0  29593  upgredgss  29597  umgredgss  29598  edgupgr  29599  uhgrvtxedgiedgb  29601  upgredg  29602  lfuhgr  29613  usgredgss  29627  ausgrumgri  29635  ausgrusgri  29636  uspgrf1oedg  29641  uspgrupgrushgr  29647  usgrumgruspgr  29650  usgruspgrb  29651  usgrf1oedg  29675  uhgr2edg  29676  usgrsizedg  29683  usgredg3  29684  ushgredgedg  29697  ushgredgedgloop  29699  usgr1e  29713  edg0usgr  29721  usgr1v0edg  29725  usgrexmpledg  29730  subgrprop3  29744  0grsubgr  29746  0uhgrsubgr  29747  subgruhgredgd  29752  uhgrspansubgrlem  29758  uhgrspan1  29771  upgrres1  29781  usgredgffibi  29792  dfnbgr3  29806  nbupgrres  29832  usgrnbcnvfv  29833  cplgrop  29905  cusgrexi  29911  structtocusgr  29914  cusgrsize  29922  1loopgredg  29969  1egrvtxdg0  29979  umgr2v2eedg  29992  edginwlk  30102  wlkl1loop  30105  wlkvtxedg  30111  uspgr2wlkeq  30113  wlkiswwlks1  30343  wlkiswwlks2lem4  30348  wlkiswwlks2lem5  30349  wlkiswwlks2  30351  wlkiswwlksupgr2  30353  2pthon3v  30419  usgrwwlks2on  30434  umgrwwlks2on  30435  clwlkclwwlk  30480  loop1cycl  30631  dfclnbgr3  48750  isubgredgss  48789  isubgredg  48790  isuspgrim0lem  48817  upgrimtrlslem2  48829  gricushgr  48841  ushggricedg  48851  stgredg  48880  usgrexmpl1edg  48948  usgrexmpl2edg  48953  gpgedg  48969