Theorem op1stg 7959

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 4833	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6844	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2745	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4834	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6848	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3448	. . 3 ⊢ 𝑥 ∈ V
8		vex 3448	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7955	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3537	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4591  ‘cfv 6499  1^st c1st 7945

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6452  df-fun 6501  df-fv 6507  df-1st 7947

This theorem is referenced by:  ot1stg  7961  ot2ndg  7962  br1steqg  7969  1stconst  8056  mposn  8059  curry2  8063  opco1  8079  mpoxopn0yelv  8169  mpoxopoveq  8175  xpmapenlem  9085  1stinl  9858  1stinr  9860  fpwwe  10577  addpipq  10868  mulpipq  10871  ordpipq  10873  swrdval  14586  ruclem1  16176  qnumdenbi  16691  setsstruct  17123  oppccofval  17658  funcf2  17811  cofuval2  17830  resfval2  17836  resf1st  17837  isnat  17893  fucco  17908  homadm  17983  setcco  18026  estrcco  18072  xpcco  18125  xpchom2  18128  xpcco2  18129  evlf2  18160  curfval  18165  curf1cl  18170  uncf1  18178  uncf2  18179  diag11  18185  diag12  18186  diag2  18187  hof2fval  18197  yonedalem21  18215  yonedalem22  18220  mvmulfval  22463  imasdsf1olem  24295  ovolicc1  25451  ioombl1lem3  25495  ioombl1lem4  25496  addsqnreup  27388  addsval  27910  mulsval  28053  brcgr  28881  opvtxfv  28985  fgreu  32647  fsuppcurry2  32700  erlbrd  33231  rlocaddval  33236  rlocmulval  33237  fracerl  33273  sategoelfvb  35400  prv1n  35412  fvtransport  36014  bj-inftyexpiinv  37190  bj-finsumval0  37267  poimirlem17  37625  poimirlem24  37632  poimirlem27  37635  rngoablo2  37897  dvhopvadd  41081  dvhopvsca  41090  dvhopaddN  41102  dvhopspN  41103  etransclem44  46270  ovnsubaddlem1  46562  ovnlecvr2  46602  ovolval5lem2  46645  gpgedgiov  48050  gpgedg2ov  48051  gpgedg2iv  48052  rngccoALTV  48253  ringccoALTV  48287  func1st  49060  oppf1st2nd  49114  upfval3  49161  swapf1val  49250  fucofval  49302  fuco111  49313  fuco21  49319  fucoid  49331  precofval3  49354  prcofvala  49360  prcofval  49361  lanfval  49596  ranfval  49597