Theorem op1stg 7933

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 4822	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6826	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2747	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4823	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6830	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3440	. . 3 ⊢ 𝑥 ∈ V
8		vex 3440	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7929	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3525	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ⟨cop 4579  ‘cfv 6481  1^st c1st 7919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6437  df-fun 6483  df-fv 6489  df-1st 7921

This theorem is referenced by:  ot1stg  7935  ot2ndg  7936  br1steqg  7943  1stconst  8030  mposn  8033  curry2  8037  opco1  8053  mpoxopn0yelv  8143  mpoxopoveq  8149  xpmapenlem  9057  1stinl  9820  1stinr  9822  fpwwe  10537  addpipq  10828  mulpipq  10831  ordpipq  10833  swrdval  14551  ruclem1  16140  qnumdenbi  16655  setsstruct  17087  oppccofval  17622  funcf2  17775  cofuval2  17794  resfval2  17800  resf1st  17801  isnat  17857  fucco  17872  homadm  17947  setcco  17990  estrcco  18036  xpcco  18089  xpchom2  18092  xpcco2  18093  evlf2  18124  curfval  18129  curf1cl  18134  uncf1  18142  uncf2  18143  diag11  18149  diag12  18150  diag2  18151  hof2fval  18161  yonedalem21  18179  yonedalem22  18184  mvmulfval  22457  imasdsf1olem  24288  ovolicc1  25444  ioombl1lem3  25488  ioombl1lem4  25489  addsqnreup  27381  addsval  27905  mulsval  28048  brcgr  28878  opvtxfv  28982  fgreu  32654  fsuppcurry2  32708  erlbrd  33230  rlocaddval  33235  rlocmulval  33236  fracerl  33272  sategoelfvb  35463  prv1n  35475  fvtransport  36076  bj-inftyexpiinv  37252  bj-finsumval0  37329  poimirlem17  37676  poimirlem24  37683  poimirlem27  37686  rngoablo2  37948  dvhopvadd  41191  dvhopvsca  41200  dvhopaddN  41212  dvhopspN  41213  etransclem44  46375  ovnsubaddlem1  46667  ovnlecvr2  46707  ovolval5lem2  46750  gpgedgiov  48164  gpgedg2ov  48165  gpgedg2iv  48166  rngccoALTV  48370  ringccoALTV  48404  func1st  49177  oppf1st2nd  49231  upfval3  49278  swapf1val  49367  fucofval  49419  fuco111  49430  fuco21  49436  fucoid  49448  precofval3  49471  prcofvala  49477  prcofval  49478  lanfval  49713  ranfval  49714