Theorem op1stg 7980

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 4837	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6862	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2745	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4838	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6866	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3451	. . 3 ⊢ 𝑥 ∈ V
8		vex 3451	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7976	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3540	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4595  ‘cfv 6511  1^st c1st 7966

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fv 6519  df-1st 7968

This theorem is referenced by:  ot1stg  7982  ot2ndg  7983  br1steqg  7990  1stconst  8079  mposn  8082  curry2  8086  opco1  8102  mpoxopn0yelv  8192  mpoxopoveq  8198  xpmapenlem  9108  1stinl  9880  1stinr  9882  fpwwe  10599  addpipq  10890  mulpipq  10893  ordpipq  10895  swrdval  14608  ruclem1  16199  qnumdenbi  16714  setsstruct  17146  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  22429  imasdsf1olem  24261  ovolicc1  25417  ioombl1lem3  25461  ioombl1lem4  25462  addsqnreup  27354  addsval  27869  mulsval  28012  brcgr  28827  opvtxfv  28931  fgreu  32596  fsuppcurry2  32649  erlbrd  33214  rlocaddval  33219  rlocmulval  33220  fracerl  33256  sategoelfvb  35406  prv1n  35418  fvtransport  36020  bj-inftyexpiinv  37196  bj-finsumval0  37273  poimirlem17  37631  poimirlem24  37638  poimirlem27  37641  rngoablo2  37903  dvhopvadd  41087  dvhopvsca  41096  dvhopaddN  41108  dvhopspN  41109  etransclem44  46276  ovnsubaddlem1  46568  ovnlecvr2  46608  ovolval5lem2  46651  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  rngccoALTV  48259  ringccoALTV  48293  func1st  49066  oppf1st2nd  49120  upfval3  49167  swapf1val  49256  fucofval  49308  fuco111  49319  fuco21  49325  fucoid  49337  precofval3  49360  prcofvala  49366  prcofval  49367  lanfval  49602  ranfval  49603