Theorem op1stg 7949

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 4817	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6840	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2753	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4818	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6844	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3434	. . 3 ⊢ 𝑥 ∈ V
8		vex 3434	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7945	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3518	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4574  ‘cfv 6494  1^st c1st 7935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5372  ax-un 7684

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-iota 6450  df-fun 6496  df-fv 6502  df-1st 7937

This theorem is referenced by:  ot1stg  7951  ot2ndg  7952  br1steqg  7959  1stconst  8045  mposn  8048  curry2  8052  opco1  8068  mpoxopn0yelv  8158  mpoxopoveq  8164  xpmapenlem  9077  1stinl  9846  1stinr  9848  fpwwe  10564  addpipq  10855  mulpipq  10858  ordpipq  10860  swrdval  14601  ruclem1  16193  qnumdenbi  16709  setsstruct  17141  oppccofval  17677  funcf2  17830  cofuval2  17849  resfval2  17855  resf1st  17856  isnat  17912  fucco  17927  homadm  18002  setcco  18045  estrcco  18091  xpcco  18144  xpchom2  18147  xpcco2  18148  evlf2  18179  curfval  18184  curf1cl  18189  uncf1  18197  uncf2  18198  diag11  18204  diag12  18205  diag2  18206  hof2fval  18216  yonedalem21  18234  yonedalem22  18239  mvmulfval  22521  imasdsf1olem  24352  ovolicc1  25497  ioombl1lem3  25541  ioombl1lem4  25542  addsqnreup  27424  addsval  27972  mulsval  28119  brcgr  28987  opvtxfv  29091  fgreu  32763  fsuppcurry2  32817  erlbrd  33343  rlocaddval  33348  rlocmulval  33349  fracerl  33386  sategoelfvb  35621  prv1n  35633  fvtransport  36234  bj-inftyexpiinv  37542  bj-finsumval0  37619  poimirlem17  37978  poimirlem24  37985  poimirlem27  37988  rngoablo2  38250  dvhopvadd  41559  dvhopvsca  41568  dvhopaddN  41580  dvhopspN  41581  etransclem44  46730  ovnsubaddlem1  47022  ovnlecvr2  47062  ovolval5lem2  47105  gpgedgiov  48559  gpgedg2ov  48560  gpgedg2iv  48561  rngccoALTV  48765  ringccoALTV  48799  func1st  49570  oppf1st2nd  49624  upfval3  49671  swapf1val  49760  fucofval  49812  fuco111  49823  fuco21  49829  fucoid  49841  precofval3  49864  prcofvala  49870  prcofval  49871  lanfval  50106  ranfval  50107