Theorem edgval 27419

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 6774	. . . 4 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
2	1	rneqd 5847	. . 3 ⊢ (𝑔 = 𝐺 → ran (iEdg‘𝑔) = ran (iEdg‘𝐺))
3		df-edg 27418	. . 3 ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
4		fvex 6787	. . . 4 ⊢ (iEdg‘𝐺) ∈ V
5	4	rnex 7759	. . 3 ⊢ ran (iEdg‘𝐺) ∈ V
6	2, 3, 5	fvmpt 6875	. 2 ⊢ (𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
7		rn0 5835	. . . 4 ⊢ ran ∅ = ∅
8	7	a1i 11	. . 3 ⊢ (¬ 𝐺 ∈ V → ran ∅ = ∅)
9		fvprc 6766	. . . 4 ⊢ (¬ 𝐺 ∈ V → (iEdg‘𝐺) = ∅)
10	9	rneqd 5847	. . 3 ⊢ (¬ 𝐺 ∈ V → ran (iEdg‘𝐺) = ran ∅)
11		fvprc 6766	. . 3 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ∅)
12	8, 10, 11	3eqtr4rd 2789	. 2 ⊢ (¬ 𝐺 ∈ V → (Edg‘𝐺) = ran (iEdg‘𝐺))
13	6, 12	pm2.61i 182	1 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2106  Vcvv 3432  ∅c0 4256  ran crn 5590  ‘cfv 6433  iEdgciedg 27367  Edgcedg 27417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6391  df-fun 6435  df-fv 6441  df-edg 27418

This theorem is referenced by:  iedgedg  27420  edgopval  27421  edgstruct  27423  edgiedgb  27424  edg0iedg0  27425  uhgredgn0  27498  upgredgss  27502  umgredgss  27503  edgupgr  27504  uhgrvtxedgiedgb  27506  upgredg  27507  usgredgss  27529  ausgrumgri  27537  ausgrusgri  27538  uspgrf1oedg  27543  uspgrupgrushgr  27547  usgrumgruspgr  27550  usgruspgrb  27551  usgrf1oedg  27574  uhgr2edg  27575  usgrsizedg  27582  usgredg3  27583  ushgredgedg  27596  ushgredgedgloop  27598  usgr1e  27612  edg0usgr  27620  usgr1v0edg  27624  usgrexmpledg  27629  subgrprop3  27643  0grsubgr  27645  0uhgrsubgr  27646  subgruhgredgd  27651  uhgrspansubgrlem  27657  uhgrspan1  27670  upgrres1  27680  usgredgffibi  27691  dfnbgr3  27705  nbupgrres  27731  usgrnbcnvfv  27732  cplgrop  27804  cusgrexi  27810  structtocusgr  27813  cusgrsize  27821  1loopgredg  27868  1egrvtxdg0  27878  umgr2v2eedg  27891  edginwlk  28002  wlkl1loop  28005  wlkvtxedg  28011  uspgr2wlkeq  28013  wlkiswwlks1  28232  wlkiswwlks2lem4  28237  wlkiswwlks2lem5  28238  wlkiswwlks2  28240  wlkiswwlksupgr2  28242  2pthon3v  28308  umgrwwlks2on  28322  clwlkclwwlk  28366  lfuhgr  33079  loop1cycl  33099  isomushgr  45278  ushrisomgr  45293