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

Theorem op1stg 7690
Description: Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
Assertion
Ref Expression
op1stg ((𝐴𝑉𝐵𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Proof of Theorem op1stg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 4795 . . . 4 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
21fveq2d 6667 . . 3 (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3 id 22 . . 3 (𝑥 = 𝐴𝑥 = 𝐴)
42, 3eqeq12d 2834 . 2 (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5 opeq2 4796 . . 3 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
65fveqeq2d 6671 . 2 (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7 vex 3495 . . 3 𝑥 ∈ V
8 vex 3495 . . 3 𝑦 ∈ V
97, 8op1st 7686 . 2 (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
104, 6, 9vtocl2g 3569 1 ((𝐴𝑉𝐵𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  cop 4563  cfv 6348  1st c1st 7676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-iota 6307  df-fun 6350  df-fv 6356  df-1st 7678
This theorem is referenced by:  ot1stg  7692  ot2ndg  7693  br1steqg  7700  1stconst  7784  mposn  7787  curry2  7791  mpoxopn0yelv  7868  mpoxopoveq  7874  xpmapenlem  8672  1stinl  9344  1stinr  9346  fpwwe  10056  addpipq  10347  mulpipq  10350  ordpipq  10352  swrdval  13993  ruclem1  15572  qnumdenbi  16072  setsstruct  16511  oppccofval  16974  funcf2  17126  cofuval2  17145  resfval2  17151  resf1st  17152  isnat  17205  fucco  17220  homadm  17288  setcco  17331  estrcco  17368  xpcco  17421  xpchom2  17424  xpcco2  17425  evlf2  17456  curfval  17461  curf1cl  17466  uncf1  17474  uncf2  17475  diag11  17481  diag12  17482  diag2  17483  hof2fval  17493  yonedalem21  17511  yonedalem22  17516  mvmulfval  21079  imasdsf1olem  22910  ovolicc1  24044  ioombl1lem3  24088  ioombl1lem4  24089  addsqnreup  25946  brcgr  26613  opvtxfv  26716  fgreu  30345  fsuppcurry2  30388  sategoelfvb  32563  prv1n  32575  fvtransport  33390  bj-inftyexpiinv  34382  bj-finsumval0  34455  poimirlem17  34790  poimirlem24  34797  poimirlem27  34800  rngoablo2  35068  dvhopvadd  38109  dvhopvsca  38118  dvhopaddN  38130  dvhopspN  38131  etransclem44  42440  ovnsubaddlem1  42729  ovnlecvr2  42769  ovolval5lem2  42812  rngccoALTV  44187  ringccoALTV  44250
  Copyright terms: Public domain W3C validator