Theorem op1stg 8024

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 4877	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6910	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2750	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4878	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6914	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3481	. . 3 ⊢ 𝑥 ∈ V
8		vex 3481	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 8020	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3573	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ⟨cop 4636  ‘cfv 6562  1^st c1st 8010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fv 6570  df-1st 8012

This theorem is referenced by:  ot1stg  8026  ot2ndg  8027  br1steqg  8034  1stconst  8123  mposn  8126  curry2  8130  opco1  8146  mpoxopn0yelv  8236  mpoxopoveq  8242  xpmapenlem  9182  1stinl  9964  1stinr  9966  fpwwe  10683  addpipq  10974  mulpipq  10977  ordpipq  10979  swrdval  14677  ruclem1  16263  qnumdenbi  16777  setsstruct  17209  oppccofval  17761  funcf2  17918  cofuval2  17937  resfval2  17943  resf1st  17944  isnat  18001  fucco  18018  homadm  18093  setcco  18136  estrcco  18184  xpcco  18238  xpchom2  18241  xpcco2  18242  evlf2  18274  curfval  18279  curf1cl  18284  uncf1  18292  uncf2  18293  diag11  18299  diag12  18300  diag2  18301  hof2fval  18311  yonedalem21  18329  yonedalem22  18334  mvmulfval  22563  imasdsf1olem  24398  ovolicc1  25564  ioombl1lem3  25608  ioombl1lem4  25609  addsqnreup  27501  addsval  28009  mulsval  28149  brcgr  28929  opvtxfv  29035  fgreu  32688  fsuppcurry2  32743  erlbrd  33249  rlocaddval  33254  rlocmulval  33255  fracerl  33287  sategoelfvb  35403  prv1n  35415  fvtransport  36013  bj-inftyexpiinv  37190  bj-finsumval0  37267  poimirlem17  37623  poimirlem24  37630  poimirlem27  37633  rngoablo2  37895  dvhopvadd  41075  dvhopvsca  41084  dvhopaddN  41096  dvhopspN  41097  etransclem44  46233  ovnsubaddlem1  46525  ovnlecvr2  46565  ovolval5lem2  46608  rngccoALTV  48114  ringccoALTV  48148