Theorem edgval 26527

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 6493	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5644	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 26526	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6506	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7426	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6589	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5669	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6486	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5644	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6486	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2819	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 177	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1507   ∈ wcel 2048  Vcvv 3409  ∅c0 4173  ran crn 5401  ‘cfv 6182  iEdgciedg 26475  Edgcedg 26525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3678  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-iota 6146  df-fun 6184  df-fv 6190  df-edg 26526

This theorem is referenced by:  iedgedg  26528  edgopval  26529  edgstruct  26531  edgiedgb  26532  edg0iedg0  26533  uhgredgn0  26606  upgredgss  26610  umgredgss  26611  edgupgr  26612  uhgrvtxedgiedgb  26614  upgredg  26615  usgredgss  26637  ausgrumgri  26645  ausgrusgri  26646  uspgrf1oedg  26651  uspgrupgrushgr  26655  usgrumgruspgr  26658  usgruspgrb  26659  usgrf1oedg  26682  uhgr2edg  26683  usgrsizedg  26690  usgredg3  26691  ushgredgedg  26704  ushgredgedgloop  26706  usgr1e  26720  edg0usgr  26728  usgr1v0edg  26732  usgrexmpledg  26737  subgrprop3  26751  0grsubgr  26753  0uhgrsubgr  26754  subgruhgredgd  26759  uhgrspansubgrlem  26765  uhgrspan1  26778  upgrres1  26788  usgredgffibi  26799  dfnbgr3  26813  nbupgrres  26839  usgrnbcnvfv  26840  cplgrop  26912  cusgrexi  26918  structtocusgr  26921  cusgrsize  26929  1loopgredg  26976  1egrvtxdg0  26986  umgr2v2eedg  26999  edginwlk  27109  wlkl1loop  27112  wlkvtxedg  27118  uspgr2wlkeq  27120  wlkiswwlks1  27343  wlkiswwlks2lem4  27348  wlkiswwlks2lem5  27349  wlkiswwlks2  27351  wlkiswwlksupgr2  27353  2pthon3v  27439  umgrwwlks2on  27453  clwlkclwwlk  27498  clwlkclwwlkOLD  27499  isomushgr  43299  ushrisomgr  43314