opvtxfv - Intuitionistic Logic Explorer

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

Theorem opvtxfv 15696

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

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1373 ∈ wcel 2177 Vcvv 2773 ⟨cop 3641 × cxp 4681 ‘cfv 5280 1^st c1st 6237 Vtxcvtx 15686

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 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4170 ax-pow 4226 ax-pr 4261 ax-un 4488 ax-cnex 8036 ax-resscn 8037 ax-1re 8039 ax-addrcl 8042

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ral 2490 df-rex 2491 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-un 3174 df-in 3176 df-ss 3183 df-if 3576 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-int 3892 df-br 4052 df-opab 4114 df-mpt 4115 df-id 4348 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-rn 4694 df-res 4695 df-iota 5241 df-fun 5282 df-fn 5283 df-f 5284 df-fo 5286 df-fv 5288 df-1st 6239 df-inn 9057 df-ndx 12910 df-slot 12911 df-base 12913 df-vtx 15688

This theorem is referenced by: opvtxov 15697 opvtxfvi 15701 gropd 15721 isuhgropm 15752 uhgrunop 15758 upgrop 15775 upgr1eopdc 15791 upgrunop 15793 umgrunop 15795

W3C validator