Theorem edgval 28574

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 6892	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5938	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 28573	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6905	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7907	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6999	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5926	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6884	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5938	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6884	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2781	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 182	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2104  Vcvv 3472  ∅c0 4323  ran crn 5678  ‘cfv 6544  iEdgciedg 28522  Edgcedg 28572

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fv 6552  df-edg 28573

This theorem is referenced by:  iedgedg  28575  edgopval  28576  edgstruct  28578  edgiedgb  28579  edg0iedg0  28580  uhgredgn0  28653  upgredgss  28657  umgredgss  28658  edgupgr  28659  uhgrvtxedgiedgb  28661  upgredg  28662  usgredgss  28684  ausgrumgri  28692  ausgrusgri  28693  uspgrf1oedg  28698  uspgrupgrushgr  28702  usgrumgruspgr  28705  usgruspgrb  28706  usgrf1oedg  28729  uhgr2edg  28730  usgrsizedg  28737  usgredg3  28738  ushgredgedg  28751  ushgredgedgloop  28753  usgr1e  28767  edg0usgr  28775  usgr1v0edg  28779  usgrexmpledg  28784  subgrprop3  28798  0grsubgr  28800  0uhgrsubgr  28801  subgruhgredgd  28806  uhgrspansubgrlem  28812  uhgrspan1  28825  upgrres1  28835  usgredgffibi  28846  dfnbgr3  28860  nbupgrres  28886  usgrnbcnvfv  28887  cplgrop  28959  cusgrexi  28965  structtocusgr  28968  cusgrsize  28976  1loopgredg  29023  1egrvtxdg0  29033  umgr2v2eedg  29046  edginwlk  29157  wlkl1loop  29160  wlkvtxedg  29166  uspgr2wlkeq  29168  wlkiswwlks1  29386  wlkiswwlks2lem4  29391  wlkiswwlks2lem5  29392  wlkiswwlks2  29394  wlkiswwlksupgr2  29396  2pthon3v  29462  umgrwwlks2on  29476  clwlkclwwlk  29520  lfuhgr  34404  loop1cycl  34424  isomushgr  46794  ushrisomgr  46809