Theorem op1stg 8026

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 4873	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6910	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2753	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4874	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6914	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3484	. . 3 ⊢ 𝑥 ∈ V
8		vex 3484	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 8022	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3574	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ⟨cop 4632  ‘cfv 6561  1^st c1st 8012

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014

This theorem is referenced by:  ot1stg  8028  ot2ndg  8029  br1steqg  8036  1stconst  8125  mposn  8128  curry2  8132  opco1  8148  mpoxopn0yelv  8238  mpoxopoveq  8244  xpmapenlem  9184  1stinl  9967  1stinr  9969  fpwwe  10686  addpipq  10977  mulpipq  10980  ordpipq  10982  swrdval  14681  ruclem1  16267  qnumdenbi  16781  setsstruct  17213  oppccofval  17759  funcf2  17913  cofuval2  17932  resfval2  17938  resf1st  17939  isnat  17995  fucco  18010  homadm  18085  setcco  18128  estrcco  18174  xpcco  18228  xpchom2  18231  xpcco2  18232  evlf2  18263  curfval  18268  curf1cl  18273  uncf1  18281  uncf2  18282  diag11  18288  diag12  18289  diag2  18290  hof2fval  18300  yonedalem21  18318  yonedalem22  18323  mvmulfval  22548  imasdsf1olem  24383  ovolicc1  25551  ioombl1lem3  25595  ioombl1lem4  25596  addsqnreup  27487  addsval  27995  mulsval  28135  brcgr  28915  opvtxfv  29021  fgreu  32682  fsuppcurry2  32737  erlbrd  33267  rlocaddval  33272  rlocmulval  33273  fracerl  33308  sategoelfvb  35424  prv1n  35436  fvtransport  36033  bj-inftyexpiinv  37209  bj-finsumval0  37286  poimirlem17  37644  poimirlem24  37651  poimirlem27  37654  rngoablo2  37916  dvhopvadd  41095  dvhopvsca  41104  dvhopaddN  41116  dvhopspN  41117  etransclem44  46293  ovnsubaddlem1  46585  ovnlecvr2  46625  ovolval5lem2  46668  rngccoALTV  48187  ringccoALTV  48221  upfval3  48935  swapf1val  48973  fucofval  49014  fuco111  49025  fuco21  49031  fucoid  49043  precoffunc  49066