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

Theorem op1stg 7934
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 4831 . . . 4 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
21fveq2d 6847 . . 3 (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3 id 22 . . 3 (𝑥 = 𝐴𝑥 = 𝐴)
42, 3eqeq12d 2753 . 2 (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5 opeq2 4832 . . 3 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
65fveqeq2d 6851 . 2 (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7 vex 3450 . . 3 𝑥 ∈ V
8 vex 3450 . . 3 𝑦 ∈ V
97, 8op1st 7930 . 2 (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
104, 6, 9vtocl2g 3532 1 ((𝐴𝑉𝐵𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  cop 4593  cfv 6497  1st c1st 7920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fv 6505  df-1st 7922
This theorem is referenced by:  ot1stg  7936  ot2ndg  7937  br1steqg  7944  1stconst  8033  mposn  8036  curry2  8040  opco1  8056  mpoxopn0yelv  8145  mpoxopoveq  8151  xpmapenlem  9089  1stinl  9864  1stinr  9866  fpwwe  10583  addpipq  10874  mulpipq  10877  ordpipq  10879  swrdval  14532  ruclem1  16114  qnumdenbi  16620  setsstruct  17049  oppccofval  17598  funcf2  17755  cofuval2  17774  resfval2  17780  resf1st  17781  isnat  17835  fucco  17852  homadm  17927  setcco  17970  estrcco  18018  xpcco  18072  xpchom2  18075  xpcco2  18076  evlf2  18108  curfval  18113  curf1cl  18118  uncf1  18126  uncf2  18127  diag11  18133  diag12  18134  diag2  18135  hof2fval  18145  yonedalem21  18163  yonedalem22  18168  mvmulfval  21894  imasdsf1olem  23729  ovolicc1  24883  ioombl1lem3  24927  ioombl1lem4  24928  addsqnreup  26794  addsval  27277  brcgr  27852  opvtxfv  27958  fgreu  31591  fsuppcurry2  31646  sategoelfvb  34016  prv1n  34028  mulsval  34411  fvtransport  34620  bj-inftyexpiinv  35682  bj-finsumval0  35759  poimirlem17  36098  poimirlem24  36105  poimirlem27  36108  rngoablo2  36371  dvhopvadd  39559  dvhopvsca  39568  dvhopaddN  39580  dvhopspN  39581  etransclem44  44526  ovnsubaddlem1  44818  ovnlecvr2  44858  ovolval5lem2  44901  rngccoALTV  46293  ringccoALTV  46356
  Copyright terms: Public domain W3C validator