opiedgfv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > opiedgfv		Structured version Visualization version GIF version

Theorem opiedgfv 27280

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 5620	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opiedgval 27279	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (iEdg‘⟨𝑉, 𝐸⟩) = (2^nd ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 17	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = (2^nd ‘⟨𝑉, 𝐸⟩))
4		op2ndg 7817	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (2^nd ‘⟨𝑉, 𝐸⟩) = 𝐸)
5	3, 4	eqtrd 2778	1 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2108 Vcvv 3422 ⟨cop 4564 × cxp 5578 ‘cfv 6418 2^nd c2nd 7803 iEdgciedg 27270

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-iota 6376 df-fun 6420 df-fv 6426 df-2nd 7805 df-iedg 27272

This theorem is referenced by: opiedgov 27281 opiedgfvi 27283 gropd 27304 edgopval 27324 isuhgrop 27343 uhgrunop 27348 upgrop 27367 upgr0eop 27387 upgr1eop 27388 upgrunop 27392 umgrunop 27394 isuspgrop 27434 isusgrop 27435 ausgrusgrb 27438 usgr0eop 27516 uspgr1eop 27517 usgr1eop 27520 usgrexmpllem 27530 uhgrspan1lem3 27572 upgrres1lem3 27582 fusgrfisbase 27598 fusgrfisstep 27599 usgrexi 27711 cusgrexi 27713 p1evtxdeqlem 27782 p1evtxdeq 27783 p1evtxdp1 27784 uspgrloopiedg 27787 umgr2v2eiedg 27793 wlk2v2e 28422 eupthvdres 28500 eupth2lemb 28502 konigsbergiedg 28512 strisomgrop 45180 ushrisomgr 45181

W3C validator