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 29063

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 Vcvv 3441 ⟨cop 4587 × cxp 5623 ‘cfv 6493 2^nd c2nd 7934 iEdgciedg 29053

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5242 ax-nul 5252 ax-pr 5378 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-rab 3401 df-v 3443 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4287 df-if 4481 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-br 5100 df-opab 5162 df-mpt 5181 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-iota 6449 df-fun 6495 df-fv 6501 df-2nd 7936 df-iedg 29055

This theorem is referenced by: opiedgov 29064 opiedgfvi 29066 gropd 29087 edgopval 29107 isuhgrop 29126 uhgrunop 29131 upgrop 29150 upgr0eop 29170 upgr1eop 29171 upgrunop 29175 umgrunop 29177 isuspgrop 29217 isusgrop 29218 ausgrusgrb 29221 usgr0eop 29302 uspgr1eop 29303 usgr1eop 29306 usgrexmpllem 29316 uhgrspan1lem3 29358 upgrres1lem3 29368 fusgrfisbase 29384 fusgrfisstep 29385 usgrexi 29497 cusgrexi 29499 p1evtxdeqlem 29569 p1evtxdeq 29570 p1evtxdp1 29571 uspgrloopiedg 29574 umgr2v2eiedg 29580 wlk2v2e 30215 eupthvdres 30293 eupth2lemb 30295 konigsbergiedg 30305 isubgriedg 48145 opstrgric 48208 ushggricedg 48209 usgrexmpl1edg 48306 usgrexmpl2edg 48311

W3C validator