Theorem edgval 29632

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 6885	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5919	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 29631	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6898	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7922	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6993	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5907	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6877	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5919	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6877	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2806	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 184	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ∅c0 4278  ran crn 5651  ‘cfv 6538  iEdgciedg 29580  Edgcedg 29630

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-edg 29631

This theorem is used by:  iedgedg  29633  edgopval  29634  edgstruct  29636  edgiedgb  29637  edg0iedg0  29638  uhgredgn0  29711  upgredgss  29715  umgredgss  29716  edgupgr  29717  uhgrvtxedgiedgb  29719  upgredg  29720  lfuhgr  29731  usgredgss  29745  ausgrumgri  29753  ausgrusgri  29754  uspgrf1oedg  29759  uspgrupgrushgr  29765  usgrumgruspgr  29768  usgruspgrb  29769  usgrf1oedg  29793  uhgr2edg  29794  usgrsizedg  29801  usgredg3  29802  ushgredgedg  29815  ushgredgedgloop  29817  usgr1e  29831  edg0usgr  29839  usgr1v0edg  29843  usgrexmpledg  29848  subgrprop3  29862  0grsubgr  29864  0uhgrsubgr  29865  subgruhgredgd  29870  uhgrspansubgrlem  29876  uhgrspan1  29889  upgrres1  29899  usgredgffibi  29910  dfnbgr3  29924  nbupgrres  29950  usgrnbcnvfv  29951  cplgrop  30023  cusgrexi  30029  structtocusgr  30032  cusgrsize  30040  1loopgredg  30087  1egrvtxdg0  30097  umgr2v2eedg  30110  edginwlk  30220  wlkl1loop  30223  wlkvtxedg  30229  uspgr2wlkeq  30231  wlkiswwlks1  30461  wlkiswwlks2lem4  30466  wlkiswwlks2lem5  30467  wlkiswwlks2  30469  wlkiswwlksupgr2  30471  2pthon3v  30537  usgrwwlks2on  30552  umgrwwlks2on  30553  clwlkclwwlk  30598  loop1cycl  30749  dfclnbgr3  49017  isubgredgss  49056  isubgredg  49057  isuspgrim0lem  49084  upgrimtrlslem2  49096  gricushgr  49108  ushggricedg  49118  stgredg  49147  usgrexmpl1edg  49215  usgrexmpl2edg  49220  gpgedg  49236