Theorem op1stg 7998

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 4849	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6879	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2751	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4850	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6883	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3463	. . 3 ⊢ 𝑥 ∈ V
8		vex 3463	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7994	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3553	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ⟨cop 4607  ‘cfv 6530  1^st c1st 7984

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fv 6538  df-1st 7986

This theorem is referenced by:  ot1stg  8000  ot2ndg  8001  br1steqg  8008  1stconst  8097  mposn  8100  curry2  8104  opco1  8120  mpoxopn0yelv  8210  mpoxopoveq  8216  xpmapenlem  9156  1stinl  9939  1stinr  9941  fpwwe  10658  addpipq  10949  mulpipq  10952  ordpipq  10954  swrdval  14659  ruclem1  16247  qnumdenbi  16761  setsstruct  17193  oppccofval  17726  funcf2  17879  cofuval2  17898  resfval2  17904  resf1st  17905  isnat  17961  fucco  17976  homadm  18051  setcco  18094  estrcco  18140  xpcco  18193  xpchom2  18196  xpcco2  18197  evlf2  18228  curfval  18233  curf1cl  18238  uncf1  18246  uncf2  18247  diag11  18253  diag12  18254  diag2  18255  hof2fval  18265  yonedalem21  18283  yonedalem22  18288  mvmulfval  22478  imasdsf1olem  24310  ovolicc1  25467  ioombl1lem3  25511  ioombl1lem4  25512  addsqnreup  27404  addsval  27912  mulsval  28052  brcgr  28825  opvtxfv  28929  fgreu  32596  fsuppcurry2  32649  erlbrd  33204  rlocaddval  33209  rlocmulval  33210  fracerl  33246  sategoelfvb  35387  prv1n  35399  fvtransport  35996  bj-inftyexpiinv  37172  bj-finsumval0  37249  poimirlem17  37607  poimirlem24  37614  poimirlem27  37617  rngoablo2  37879  dvhopvadd  41058  dvhopvsca  41067  dvhopaddN  41079  dvhopspN  41080  etransclem44  46255  ovnsubaddlem1  46547  ovnlecvr2  46587  ovolval5lem2  46630  rngccoALTV  48194  ringccoALTV  48228  oppf1st2nd  49027  upfval3  49061  swapf1val  49132  fucofval  49178  fuco111  49189  fuco21  49195  fucoid  49207  precofval3  49230  prcofvala  49236  prcofval  49237  lanfval  49438  ranfval  49439