Theorem opiedgfv 29215

Description: The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.)

Assertion

Ref	Expression
opiedgfv	⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸)

Proof of Theorem opiedgfv

Step	Hyp	Ref	Expression
1		opelvvg 5689	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opiedgval 29214	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (iEdg‘⟨𝑉, 𝐸⟩) = (2nd ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 17	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = (2nd ‘⟨𝑉, 𝐸⟩))
4		op2ndg 7983	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (2nd ‘⟨𝑉, 𝐸⟩) = 𝐸)
5	3, 4	eqtrd 2798	1 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1561   ∈ wcel 2143  Vcvv 3455  ⟨cop 4589   × cxp 5646  ‘cfv 6521  2^nd c2nd 7969  iEdgciedg 29205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-iota 6477  df-fun 6523  df-fv 6529  df-2nd 7971  df-iedg 29207

This theorem is referenced by:  opiedgov  29216  opiedgfvi  29218  gropd  29239  edgopval  29259  isuhgrop  29278  uhgrunop  29283  upgrop  29302  upgr0eop  29322  upgr1eop  29323  upgrunop  29327  umgrunop  29329  isuspgrop  29369  isusgrop  29370  ausgrusgrb  29373  usgr0eop  29454  uspgr1eop  29455  usgr1eop  29458  usgrexmpllem  29468  uhgrspan1lem3  29510  upgrres1lem3  29520  fusgrfisbase  29536  fusgrfisstep  29537  usgrexi  29649  cusgrexi  29651  p1evtxdeqlem  29720  p1evtxdeq  29721  p1evtxdp1  29722  uspgrloopiedg  29725  umgr2v2eiedg  29731  wlk2v2e  30366  eupthvdres  30444  eupth2lemb  30446  konigsbergiedg  30456  isubgriedg  48476  opstrgric  48539  ushggricedg  48540  usgrexmpl1edg  48637  usgrexmpl2edg  48642