Theorem edgval 29436

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 6888	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5933	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29435	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6901	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7916	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6996	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5921	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6880	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5933	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6880	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2812	. 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 2146  Vcvv 3458  ∅c0 4289  ran crn 5667  ‘cfv 6543  iEdgciedg 29384  Edgcedg 29434

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fv 6551  df-edg 29435

This theorem is used by:  iedgedg  29437  edgopval  29438  edgstruct  29440  edgiedgb  29441  edg0iedg0  29442  uhgredgn0  29515  upgredgss  29519  umgredgss  29520  edgupgr  29521  uhgrvtxedgiedgb  29523  upgredg  29524  usgredgss  29546  ausgrumgri  29554  ausgrusgri  29555  uspgrf1oedg  29560  uspgrupgrushgr  29566  usgrumgruspgr  29569  usgruspgrb  29570  usgrf1oedg  29594  uhgr2edg  29595  usgrsizedg  29602  usgredg3  29603  ushgredgedg  29616  ushgredgedgloop  29618  usgr1e  29632  edg0usgr  29640  usgr1v0edg  29644  usgrexmpledg  29649  subgrprop3  29663  0grsubgr  29665  0uhgrsubgr  29666  subgruhgredgd  29671  uhgrspansubgrlem  29677  uhgrspan1  29690  upgrres1  29700  usgredgffibi  29711  dfnbgr3  29725  nbupgrres  29751  usgrnbcnvfv  29752  cplgrop  29824  cusgrexi  29830  structtocusgr  29833  cusgrsize  29841  1loopgredg  29888  1egrvtxdg0  29898  umgr2v2eedg  29911  edginwlk  30021  wlkl1loop  30024  wlkvtxedg  30030  uspgr2wlkeq  30032  wlkiswwlks1  30253  wlkiswwlks2lem4  30258  wlkiswwlks2lem5  30259  wlkiswwlks2  30261  wlkiswwlksupgr2  30263  2pthon3v  30329  usgrwwlks2on  30344  umgrwwlks2on  30345  clwlkclwwlk  30390  lfuhgr  35631  loop1cycl  35650  dfclnbgr3  48632  isubgredgss  48671  isubgredg  48672  isuspgrim0lem  48699  upgrimtrlslem2  48711  gricushgr  48723  ushggricedg  48733  stgredg  48762  usgrexmpl1edg  48830  usgrexmpl2edg  48835  gpgedg  48851