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

Theorem opvtxfv 29021
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
StepHypRef Expression
1 opelvvg 5726 . . 3 ((𝑉𝑋𝐸𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2 opvtxval 29020 . . 3 (⟨𝑉, 𝐸⟩ ∈ (V × V) → (Vtx‘⟨𝑉, 𝐸⟩) = (1st ‘⟨𝑉, 𝐸⟩))
31, 2syl 17 . 2 ((𝑉𝑋𝐸𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = (1st ‘⟨𝑉, 𝐸⟩))
4 op1stg 8026 . 2 ((𝑉𝑋𝐸𝑌) → (1st ‘⟨𝑉, 𝐸⟩) = 𝑉)
53, 4eqtrd 2777 1 ((𝑉𝑋𝐸𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  Vcvv 3480  cop 4632   × cxp 5683  cfv 6561  1st c1st 8012  Vtxcvtx 29013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014  df-vtx 29015
This theorem is referenced by:  opvtxov  29022  opvtxfvi  29026  gropd  29048  isuhgrop  29087  uhgrunop  29092  upgrop  29111  upgr1eop  29132  upgrunop  29136  umgrunop  29138  isuspgrop  29178  isusgrop  29179  ausgrusgrb  29182  uspgr1eop  29264  usgr1eop  29267  usgrexmpllem  29277  uhgrspan1lem2  29318  upgrres1lem2  29328  opfusgr  29340  fusgrfisbase  29345  fusgrfisstep  29346  usgrexi  29458  cusgrexi  29460  p1evtxdeqlem  29530  p1evtxdeq  29531  p1evtxdp1  29532  uspgrloopvtx  29533  umgr2v2evtx  29539  wlk2v2e  30176  eupthvdres  30254  eupth2lemb  30256  konigsbergvtx  30265  konigsberg  30276  isubgrvtx  47853  opstrgric  47895  ushggricedg  47896  usgrexmpl1vtx  47982  usgrexmpl2vtx  47987  uspgrsprfo  48064
  Copyright terms: Public domain W3C validator