Theorem op1stg 7957

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 4831	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6848	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2753	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4832	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6852	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3446	. . 3 ⊢ 𝑥 ∈ V
8		vex 3446	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7953	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3531	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4588  ‘cfv 6502  1^st c1st 7943

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 5245  ax-nul 5255  ax-pr 5381  ax-un 7692

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6458  df-fun 6504  df-fv 6510  df-1st 7945

This theorem is referenced by:  ot1stg  7959  ot2ndg  7960  br1steqg  7967  1stconst  8054  mposn  8057  curry2  8061  opco1  8077  mpoxopn0yelv  8167  mpoxopoveq  8173  xpmapenlem  9086  1stinl  9853  1stinr  9855  fpwwe  10571  addpipq  10862  mulpipq  10865  ordpipq  10867  swrdval  14581  ruclem1  16170  qnumdenbi  16685  setsstruct  17117  oppccofval  17653  funcf2  17806  cofuval2  17825  resfval2  17831  resf1st  17832  isnat  17888  fucco  17903  homadm  17978  setcco  18021  estrcco  18067  xpcco  18120  xpchom2  18123  xpcco2  18124  evlf2  18155  curfval  18160  curf1cl  18165  uncf1  18173  uncf2  18174  diag11  18180  diag12  18181  diag2  18182  hof2fval  18192  yonedalem21  18210  yonedalem22  18215  mvmulfval  22503  imasdsf1olem  24334  ovolicc1  25490  ioombl1lem3  25534  ioombl1lem4  25535  addsqnreup  27427  addsval  27975  mulsval  28122  brcgr  28991  opvtxfv  29095  fgreu  32767  fsuppcurry2  32821  erlbrd  33363  rlocaddval  33368  rlocmulval  33369  fracerl  33406  sategoelfvb  35641  prv1n  35653  fvtransport  36254  bj-inftyexpiinv  37490  bj-finsumval0  37567  poimirlem17  37917  poimirlem24  37924  poimirlem27  37927  rngoablo2  38189  dvhopvadd  41498  dvhopvsca  41507  dvhopaddN  41519  dvhopspN  41520  etransclem44  46665  ovnsubaddlem1  46957  ovnlecvr2  46997  ovolval5lem2  47040  gpgedgiov  48454  gpgedg2ov  48455  gpgedg2iv  48456  rngccoALTV  48660  ringccoALTV  48694  func1st  49465  oppf1st2nd  49519  upfval3  49566  swapf1val  49655  fucofval  49707  fuco111  49718  fuco21  49724  fucoid  49736  precofval3  49759  prcofvala  49765  prcofval  49766  lanfval  50001  ranfval  50002