Theorem op1stg 8013

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 4832	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6889	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 23	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2776	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4833	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6893	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3454	. . 3 ⊢ 𝑥 ∈ V
8		vex 3454	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 8009	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3533	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ⟨cop 4589  ‘cfv 6538  1^st c1st 7999

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-1st 8001

This theorem is used by:  ot1stg  8015  ot2ndg  8016  br1steqg  8023  1stconst  8111  mposn  8114  curry2  8118  opco1  8134  mpoxopn0yelv  8230  mpoxopoveq  8236  xpmapenlem  9163  1stinl  10008  1stinr  10010  fpwwe  10731  addpipq  11022  mulpipq  11025  ordpipq  11027  swrdval  14791  ruclem1  16399  qnumdenbi  16920  setsstruct  17354  oppccofval  17890  funcf2  18043  cofuval2  18062  resfval2  18068  resf1st  18069  isnat  18125  fucco  18140  homadm  18215  setcco  18258  estrcco  18304  xpcco  18357  xpchom2  18360  xpcco2  18361  evlf2  18392  curfval  18397  curf1cl  18402  uncf1  18410  uncf2  18411  diag11  18417  diag12  18418  diag2  18419  hof2fval  18429  yonedalem21  18447  yonedalem22  18452  mvmulfval  22857  imasdsf1olem  24692  ovolicc1  25837  ioombl1lem3  25881  ioombl1lem4  25882  addsqnreup  27770  addsval  28348  mulsval  28495  brcgr  29478  opvtxfv  29582  fgreu  33307  fsuppcurry2  33359  erlbrd  33866  erld2  33869  rlocaddval  33872  rlocmulval  33873  fracerl  33910  sategoelfvb  36226  prv1n  36238  fvtransport  36839  bj-inftyexpiinv  38172  bj-finsumval0  38249  poimirlem17  38598  poimirlem24  38605  poimirlem27  38608  rngoablo2  38886  dvhopvadd  42193  dvhopvsca  42202  dvhopaddN  42214  dvhopspN  42215  etransclem44  47331  ovnsubaddlem1  47623  ovnlecvr2  47663  ovolval5lem2  47706  gpgedgiov  49206  gpgedg2ov  49207  gpgedg2iv  49208  rngccoALTV  49411  ringccoALTV  49445  func1st  50228  oppf1st2nd  50282  upfval3  50329  swapf1val  50418  fucofval  50470  fuco111  50481  fuco21  50487  fucoid  50499  precofval3  50522  prcofvala  50528  prcofval  50529  lanfval  50764  ranfval  50765