Theorem op1stg 8034

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 4843	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6909	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 23	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2779	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4844	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6913	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3458	. . 3 ⊢ 𝑥 ∈ V
8		vex 3458	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 8030	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3537	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ⟨cop 4838  ‘cfv 6555  1^st c1st 8020

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6509  df-fun 6557  df-fv 6563  df-1st 8022

This theorem is used by:  ot1stg  8036  ot2ndg  8037  br1steqg  8044  1stconst  8135  mposn  8138  curry2  8142  opco1  8158  mpoxopn0yelv  8255  mpoxopoveq  8261  xpmapenlem  9188  1stinl  10032  1stinr  10034  fpwwe  10755  addpipq  11046  mulpipq  11049  ordpipq  11051  swrdval  14816  ruclem1  16425  qnumdenbi  16946  setsstruct  17380  oppccofval  17916  funcf2  18069  cofuval2  18088  resfval2  18094  resf1st  18095  isnat  18151  fucco  18166  homadm  18241  setcco  18284  estrcco  18330  xpcco  18383  xpchom2  18386  xpcco2  18387  evlf2  18418  curfval  18423  curf1cl  18428  uncf1  18436  uncf2  18437  diag11  18443  diag12  18444  diag2  18445  hof2fval  18455  yonedalem21  18473  yonedalem22  18478  mvmulfval  22884  imasdsf1olem  24719  ovolicc1  25864  ioombl1lem3  25908  ioombl1lem4  25909  addsqnreup  27797  addsval  28375  mulsval  28522  brcgr  29505  opvtxfv  29609  fgreu  33334  fsuppcurry2  33384  erlbrd  33891  erld2  33894  rlocaddval  33897  rlocmulval  33898  fracerl  33935  brlexod  35998  brr0d  36000  sategoelfvb  36350  prv1n  36362  fvtransport  36974  bj-inftyexpiinv  38320  bj-finsumval0  38397  poimirlem17  38746  poimirlem24  38753  poimirlem27  38756  rngoablo2  39034  dvhopvadd  42341  dvhopvsca  42350  dvhopaddN  42362  dvhopspN  42363  etransclem44  47491  ovnsubaddlem1  47783  ovnlecvr2  47823  ovolval5lem2  47866  gpgedgiov  49366  gpgedg2ov  49367  gpgedg2iv  49368  rngccoALTV  49571  ringccoALTV  49605  func1st  50394  ixpovf  50400  oppf1st2nd  50450  upfval3  50497  swapf1val  50592  fucofval  50644  fuco111  50655  fuco21  50661  fucoid  50673  precofval3  50709  prcofvala  50715  prcofval  50716  lanfval  50999  ranfval  51000