opvtxfv - Metamath Proof Explorer

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

Theorem opvtxfv 29081

Description: The set of vertices 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
opvtxfv	⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉)

**Proof of Theorem opvtxfv**
Step	Hyp	Ref	Expression
1		opelvvg 5666	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opvtxval 29080	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 17	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
4		op1stg 7947	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (1^st ‘⟨𝑉, 𝐸⟩) = 𝑉)
5	3, 4	eqtrd 2772	1 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 Vcvv 3441 ⟨cop 4587 × cxp 5623 ‘cfv 6493 1^st c1st 7933 Vtxcvtx 29073

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-1st 7935 df-vtx 29075

This theorem is referenced by: opvtxov 29082 opvtxfvi 29086 gropd 29108 isuhgrop 29147 uhgrunop 29152 upgrop 29171 upgr1eop 29192 upgrunop 29196 umgrunop 29198 isuspgrop 29238 isusgrop 29239 ausgrusgrb 29242 uspgr1eop 29324 usgr1eop 29327 usgrexmpllem 29337 uhgrspan1lem2 29378 upgrres1lem2 29388 opfusgr 29400 fusgrfisbase 29405 fusgrfisstep 29406 usgrexi 29518 cusgrexi 29520 p1evtxdeqlem 29590 p1evtxdeq 29591 p1evtxdp1 29592 uspgrloopvtx 29593 umgr2v2evtx 29599 wlk2v2e 30236 eupthvdres 30314 eupth2lemb 30316 konigsbergvtx 30325 konigsberg 30336 isubgrvtx 48180 opstrgric 48239 ushggricedg 48240 usgrexmpl1vtx 48336 usgrexmpl2vtx 48341 uspgrsprfo 48461

W3C validator