Theorem op1stg 8013

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.

Step	Hyp	Ref	Expression
1		opeq1 4832	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6889	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 23	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2776	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4833	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6893	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3454	. . 3 ⊢ 𝑥 ∈ V
8		vex 3454	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 8009	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3533	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ⟨cop 4589  ‘cfv 6538  1^st c1st 7999

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-1st 8001

This theorem is used by:  ot1stg  8015  ot2ndg  8016  br1steqg  8023  1stconst  8111  mposn  8114  curry2  8118  opco1  8134  mpoxopn0yelv  8230  mpoxopoveq  8236  xpmapenlem  9163  1stinl  10008  1stinr  10010  fpwwe  10731  addpipq  11022  mulpipq  11025  ordpipq  11027  swrdval  14791  ruclem1  16399  qnumdenbi  16920  setsstruct  17354  oppccofval  17890  funcf2  18043  cofuval2  18062  resfval2  18068  resf1st  18069  isnat  18125  fucco  18140  homadm  18215  setcco  18258  estrcco  18304  xpcco  18357  xpchom2  18360  xpcco2  18361  evlf2  18392  curfval  18397  curf1cl  18402  uncf1  18410  uncf2  18411  diag11  18417  diag12  18418  diag2  18419  hof2fval  18429  yonedalem21  18447  yonedalem22  18452  mvmulfval  22857  imasdsf1olem  24692  ovolicc1  25837  ioombl1lem3  25881  ioombl1lem4  25882  addsqnreup  27770  addsval  28348  mulsval  28495  brcgr  29478  opvtxfv  29582  fgreu  33265  fsuppcurry2  33317  erlbrd  33824  erld2  33827  rlocaddval  33830  rlocmulval  33831  fracerl  33868  sategoelfvb  36184  prv1n  36196  fvtransport  36797  bj-inftyexpiinv  38130  bj-finsumval0  38207  poimirlem17  38556  poimirlem24  38563  poimirlem27  38566  rngoablo2  38844  dvhopvadd  42151  dvhopvsca  42160  dvhopaddN  42172  dvhopspN  42173  etransclem44  47288  ovnsubaddlem1  47580  ovnlecvr2  47620  ovolval5lem2  47663  gpgedgiov  49163  gpgedg2ov  49164  gpgedg2iv  49165  rngccoALTV  49368  ringccoALTV  49402  func1st  50185  oppf1st2nd  50239  upfval3  50286  swapf1val  50375  fucofval  50427  fuco111  50438  fuco21  50444  fucoid  50456  precofval3  50479  prcofvala  50485  prcofval  50486  lanfval  50721  ranfval  50722