Theorem edgval 27094

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 6695	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5792	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 27093	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6708	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7668	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6796	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5780	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6687	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5792	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6687	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2782	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 185	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1543   ∈ wcel 2112  Vcvv 3398  ∅c0 4223  ran crn 5537  ‘cfv 6358  iEdgciedg 27042  Edgcedg 27092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-iota 6316  df-fun 6360  df-fv 6366  df-edg 27093

This theorem is referenced by:  iedgedg  27095  edgopval  27096  edgstruct  27098  edgiedgb  27099  edg0iedg0  27100  uhgredgn0  27173  upgredgss  27177  umgredgss  27178  edgupgr  27179  uhgrvtxedgiedgb  27181  upgredg  27182  usgredgss  27204  ausgrumgri  27212  ausgrusgri  27213  uspgrf1oedg  27218  uspgrupgrushgr  27222  usgrumgruspgr  27225  usgruspgrb  27226  usgrf1oedg  27249  uhgr2edg  27250  usgrsizedg  27257  usgredg3  27258  ushgredgedg  27271  ushgredgedgloop  27273  usgr1e  27287  edg0usgr  27295  usgr1v0edg  27299  usgrexmpledg  27304  subgrprop3  27318  0grsubgr  27320  0uhgrsubgr  27321  subgruhgredgd  27326  uhgrspansubgrlem  27332  uhgrspan1  27345  upgrres1  27355  usgredgffibi  27366  dfnbgr3  27380  nbupgrres  27406  usgrnbcnvfv  27407  cplgrop  27479  cusgrexi  27485  structtocusgr  27488  cusgrsize  27496  1loopgredg  27543  1egrvtxdg0  27553  umgr2v2eedg  27566  edginwlk  27676  wlkl1loop  27679  wlkvtxedg  27685  uspgr2wlkeq  27687  wlkiswwlks1  27905  wlkiswwlks2lem4  27910  wlkiswwlks2lem5  27911  wlkiswwlks2  27913  wlkiswwlksupgr2  27915  2pthon3v  27981  umgrwwlks2on  27995  clwlkclwwlk  28039  lfuhgr  32746  loop1cycl  32766  isomushgr  44894  ushrisomgr  44909