opvtxfv - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > opvtxfv		GIF version

Theorem opvtxfv 15860

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 4771	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opvtxval 15859	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 14	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
4		op1stg 6306	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (1^st ‘⟨𝑉, 𝐸⟩) = 𝑉)
5	3, 4	eqtrd 2262	1 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1395 ∈ wcel 2200 Vcvv 2800 ⟨cop 3670 × cxp 4719 ‘cfv 5322 1^st c1st 6294 Vtxcvtx 15850

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4203 ax-pow 4260 ax-pr 4295 ax-un 4526 ax-cnex 8111 ax-resscn 8112 ax-1re 8114 ax-addrcl 8117

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-rab 2517 df-v 2802 df-sbc 3030 df-csb 3126 df-un 3202 df-in 3204 df-ss 3211 df-if 3604 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3890 df-int 3925 df-br 4085 df-opab 4147 df-mpt 4148 df-id 4386 df-xp 4727 df-rel 4728 df-cnv 4729 df-co 4730 df-dm 4731 df-rn 4732 df-res 4733 df-iota 5282 df-fun 5324 df-fn 5325 df-f 5326 df-fo 5328 df-fv 5330 df-1st 6296 df-inn 9132 df-ndx 13072 df-slot 13073 df-base 13075 df-vtx 15852

This theorem is referenced by: opvtxov 15861 opvtxfvi 15865 gropd 15885 isuhgropm 15918 uhgrunop 15924 upgrop 15941 upgr1eopdc 15960 upgrunop 15962 umgrunop 15964 isuspgropen 15999 isusgropen 16000 ausgrusgrben 16003 uspgr1eopdc 16078 usgr1eop 16080 vtxdgop 16094

W3C validator