opvtxfv - Intuitionistic Logic Explorer

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

Theorem opvtxfv 15863

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 4773	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opvtxval 15862	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 14	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
4		op1stg 6308	. 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 4721 ‘cfv 5324 1^st c1st 6296 Vtxcvtx 15853

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 4205 ax-pow 4262 ax-pr 4297 ax-un 4528 ax-cnex 8113 ax-resscn 8114 ax-1re 8116 ax-addrcl 8119

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 3892 df-int 3927 df-br 4087 df-opab 4149 df-mpt 4150 df-id 4388 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-fo 5330 df-fv 5332 df-1st 6298 df-inn 9134 df-ndx 13075 df-slot 13076 df-base 13078 df-vtx 15855

This theorem is referenced by: opvtxov 15864 opvtxfvi 15868 gropd 15888 isuhgropm 15922 uhgrunop 15928 upgrop 15945 upgr1eopdc 15964 upgrunop 15966 umgrunop 15968 isuspgropen 16003 isusgropen 16004 ausgrusgrben 16007 uspgr1eopdc 16082 usgr1eop 16084 vtxdgop 16098

W3C validator