Theorem op2ndg 8027

Description: Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)

Assertion

Ref	Expression
op2ndg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Proof of Theorem op2ndg

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq1 4873	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6914	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4874	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6910	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2753	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3484	. . 3 ⊢ 𝑥 ∈ V
8		vex 3484	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 8023	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3574	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ⟨cop 4632  ‘cfv 6561  2^nd c2nd 8013

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-2nd 8015

This theorem is referenced by:  ot2ndg  8029  ot3rdg  8030  br2ndeqg  8037  2ndconst  8126  mposn  8128  curry1  8129  opco2  8149  xpmapenlem  9184  2ndinl  9968  2ndinr  9970  axdc4lem  10495  pinq  10967  addpipq  10977  mulpipq  10980  ordpipq  10982  swrdval  14681  ruclem1  16267  eucalg  16624  qnumdenbi  16781  setsstruct  17213  comffval  17742  oppccofval  17759  funcf2  17913  cofuval2  17932  resfval2  17938  resf2nd  17940  funcres  17941  isnat  17995  fucco  18010  homacd  18086  setcco  18128  catcco  18150  estrcco  18174  xpcco  18228  xpchom2  18231  xpcco2  18232  evlf2  18263  curfval  18268  curf1cl  18273  uncf1  18281  uncf2  18282  hof2fval  18300  yonedalem21  18318  yonedalem22  18323  mvmulfval  22548  imasdsf1olem  24383  ovolicc1  25551  ioombl1lem3  25595  ioombl1lem4  25596  addsqnreup  27487  addsval  27995  mulsval  28135  om2noseqrdg  28310  brcgr  28915  opiedgfv  29024  fsuppcurry1  32736  erlbrd  33267  rlocaddval  33272  rlocmulval  33273  fracerl  33308  sategoelfvb  35424  prv1n  35436  fvtransport  36033  bj-finsumval0  37286  poimirlem17  37644  poimirlem24  37651  poimirlem27  37654  dvhopvadd  41095  dvhopvsca  41104  dvhopaddN  41116  dvhopspN  41117  etransclem44  46293  uspgrsprfo  48064  rngccoALTV  48187  ringccoALTV  48221  lmod1zr  48410  upfval3  48935  swapf2fval  48971  fucofval  49014  fuco112  49024  fuco21  49031