Theorem op1stg 7983

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 4840	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6865	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2746	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4841	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6869	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3454	. . 3 ⊢ 𝑥 ∈ V
8		vex 3454	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7979	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3543	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4598  ‘cfv 6514  1^st c1st 7969

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-1st 7971

This theorem is referenced by:  ot1stg  7985  ot2ndg  7986  br1steqg  7993  1stconst  8082  mposn  8085  curry2  8089  opco1  8105  mpoxopn0yelv  8195  mpoxopoveq  8201  xpmapenlem  9114  1stinl  9887  1stinr  9889  fpwwe  10606  addpipq  10897  mulpipq  10900  ordpipq  10902  swrdval  14615  ruclem1  16206  qnumdenbi  16721  setsstruct  17153  oppccofval  17684  funcf2  17837  cofuval2  17856  resfval2  17862  resf1st  17863  isnat  17919  fucco  17934  homadm  18009  setcco  18052  estrcco  18098  xpcco  18151  xpchom2  18154  xpcco2  18155  evlf2  18186  curfval  18191  curf1cl  18196  uncf1  18204  uncf2  18205  diag11  18211  diag12  18212  diag2  18213  hof2fval  18223  yonedalem21  18241  yonedalem22  18246  mvmulfval  22436  imasdsf1olem  24268  ovolicc1  25424  ioombl1lem3  25468  ioombl1lem4  25469  addsqnreup  27361  addsval  27876  mulsval  28019  brcgr  28834  opvtxfv  28938  fgreu  32603  fsuppcurry2  32656  erlbrd  33221  rlocaddval  33226  rlocmulval  33227  fracerl  33263  sategoelfvb  35413  prv1n  35425  fvtransport  36027  bj-inftyexpiinv  37203  bj-finsumval0  37280  poimirlem17  37638  poimirlem24  37645  poimirlem27  37648  rngoablo2  37910  dvhopvadd  41094  dvhopvsca  41103  dvhopaddN  41115  dvhopspN  41116  etransclem44  46283  ovnsubaddlem1  46575  ovnlecvr2  46615  ovolval5lem2  46658  gpgedgiov  48060  gpgedg2ov  48061  gpgedg2iv  48062  rngccoALTV  48263  ringccoALTV  48297  func1st  49070  oppf1st2nd  49124  upfval3  49171  swapf1val  49260  fucofval  49312  fuco111  49323  fuco21  49329  fucoid  49341  precofval3  49364  prcofvala  49370  prcofval  49371  lanfval  49606  ranfval  49607