Theorem op1stg 7947

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 4807	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6835	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2757	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4808	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6839	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3437	. . 3 ⊢ 𝑥 ∈ V
8		vex 3437	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7943	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3519	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ⟨cop 4564  ‘cfv 6489  1^st c1st 7933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fv 6497  df-1st 7935

This theorem is referenced by:  ot1stg  7949  ot2ndg  7950  br1steqg  7957  1stconst  8043  mposn  8046  curry2  8050  opco1  8066  mpoxopn0yelv  8157  mpoxopoveq  8163  xpmapenlem  9076  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  22529  imasdsf1olem  24360  ovolicc1  25505  ioombl1lem3  25549  ioombl1lem4  25550  addsqnreup  27428  addsval  27976  mulsval  28123  brcgr  28991  opvtxfv  29095  fgreu  32767  fsuppcurry2  32821  erlbrd  33348  rlocaddval  33353  rlocmulval  33354  fracerl  33394  sategoelfvb  35662  prv1n  35674  fvtransport  36275  bj-inftyexpiinv  37583  bj-finsumval0  37660  poimirlem17  38019  poimirlem24  38026  poimirlem27  38029  rngoablo2  38291  dvhopvadd  41600  dvhopvsca  41609  dvhopaddN  41621  dvhopspN  41622  etransclem44  46735  ovnsubaddlem1  47027  ovnlecvr2  47067  ovolval5lem2  47110  gpgedgiov  48570  gpgedg2ov  48571  gpgedg2iv  48572  rngccoALTV  48776  ringccoALTV  48810  func1st  49581  oppf1st2nd  49635  upfval3  49682  swapf1val  49771  fucofval  49823  fuco111  49834  fuco21  49840  fucoid  49852  precofval3  49875  prcofvala  49881  prcofval  49882  lanfval  50117  ranfval  50118