Theorem edgval 27517

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 6804	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5859	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 27516	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6817	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7795	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6907	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5847	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6796	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5859	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6796	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2786	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 182	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1538   ∈ wcel 2103  Vcvv 3436  ∅c0 4261  ran crn 5601  ‘cfv 6458  iEdgciedg 27465  Edgcedg 27515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-10 2134  ax-11 2151  ax-12 2168  ax-ext 2706  ax-sep 5231  ax-nul 5238  ax-pr 5360  ax-un 7621

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2727  df-clel 2813  df-nfc 2885  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3357  df-v 3438  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4844  df-br 5081  df-opab 5143  df-mpt 5164  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-iota 6410  df-fun 6460  df-fv 6466  df-edg 27516

This theorem is referenced by:  iedgedg  27518  edgopval  27519  edgstruct  27521  edgiedgb  27522  edg0iedg0  27523  uhgredgn0  27596  upgredgss  27600  umgredgss  27601  edgupgr  27602  uhgrvtxedgiedgb  27604  upgredg  27605  usgredgss  27627  ausgrumgri  27635  ausgrusgri  27636  uspgrf1oedg  27641  uspgrupgrushgr  27645  usgrumgruspgr  27648  usgruspgrb  27649  usgrf1oedg  27672  uhgr2edg  27673  usgrsizedg  27680  usgredg3  27681  ushgredgedg  27694  ushgredgedgloop  27696  usgr1e  27710  edg0usgr  27718  usgr1v0edg  27722  usgrexmpledg  27727  subgrprop3  27741  0grsubgr  27743  0uhgrsubgr  27744  subgruhgredgd  27749  uhgrspansubgrlem  27755  uhgrspan1  27768  upgrres1  27778  usgredgffibi  27789  dfnbgr3  27803  nbupgrres  27829  usgrnbcnvfv  27830  cplgrop  27902  cusgrexi  27908  structtocusgr  27911  cusgrsize  27919  1loopgredg  27966  1egrvtxdg0  27976  umgr2v2eedg  27989  edginwlk  28100  wlkl1loop  28103  wlkvtxedg  28109  uspgr2wlkeq  28111  wlkiswwlks1  28330  wlkiswwlks2lem4  28335  wlkiswwlks2lem5  28336  wlkiswwlks2  28338  wlkiswwlksupgr2  28340  2pthon3v  28406  umgrwwlks2on  28420  clwlkclwwlk  28464  lfuhgr  33175  loop1cycl  33195  isomushgr  45535  ushrisomgr  45550