Theorem op1stg 7936

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4583  ‘cfv 6482  1^st c1st 7922

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 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fv 6490  df-1st 7924

This theorem is referenced by:  ot1stg  7938  ot2ndg  7939  br1steqg  7946  1stconst  8033  mposn  8036  curry2  8040  opco1  8056  mpoxopn0yelv  8146  mpoxopoveq  8152  xpmapenlem  9061  1stinl  9823  1stinr  9825  fpwwe  10540  addpipq  10831  mulpipq  10834  ordpipq  10836  swrdval  14550  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  22427  imasdsf1olem  24259  ovolicc1  25415  ioombl1lem3  25459  ioombl1lem4  25460  addsqnreup  27352  addsval  27876  mulsval  28019  brcgr  28849  opvtxfv  28953  fgreu  32623  fsuppcurry2  32677  erlbrd  33212  rlocaddval  33217  rlocmulval  33218  fracerl  33254  sategoelfvb  35412  prv1n  35424  fvtransport  36026  bj-inftyexpiinv  37202  bj-finsumval0  37279  poimirlem17  37637  poimirlem24  37644  poimirlem27  37647  rngoablo2  37909  dvhopvadd  41092  dvhopvsca  41101  dvhopaddN  41113  dvhopspN  41114  etransclem44  46279  ovnsubaddlem1  46571  ovnlecvr2  46611  ovolval5lem2  46654  gpgedgiov  48069  gpgedg2ov  48070  gpgedg2iv  48071  rngccoALTV  48275  ringccoALTV  48309  func1st  49082  oppf1st2nd  49136  upfval3  49183  swapf1val  49272  fucofval  49324  fuco111  49335  fuco21  49341  fucoid  49353  precofval3  49376  prcofvala  49382  prcofval  49383  lanfval  49618  ranfval  49619