Theorem op2ndg 7951

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 4811	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6842	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4812	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6838	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2756	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3436	. . 3 ⊢ 𝑥 ∈ V
8		vex 3436	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7947	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3520	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ⟨cop 4568  ‘cfv 6492  2^nd c2nd 7937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fv 6500  df-2nd 7939

This theorem is referenced by:  ot2ndg  7953  ot3rdg  7954  br2ndeqg  7961  2ndconst  8047  mposn  8049  curry1  8050  opco2  8070  xpmapenlem  9079  2ndinl  9850  2ndinr  9852  axdc4lem  10375  pinq  10848  addpipq  10858  mulpipq  10861  ordpipq  10863  swrdval  14604  ruclem1  16196  eucalg  16554  qnumdenbi  16712  setsstruct  17144  comffval  17663  oppccofval  17680  funcf2  17833  cofuval2  17852  resfval2  17858  resf2nd  17860  funcres  17861  isnat  17915  fucco  17930  homacd  18006  setcco  18048  catcco  18070  estrcco  18094  xpcco  18147  xpchom2  18150  xpcco2  18151  evlf2  18182  curfval  18187  curf1cl  18192  uncf1  18200  uncf2  18201  hof2fval  18219  yonedalem21  18237  yonedalem22  18242  mvmulfval  22532  imasdsf1olem  24363  ovolicc1  25508  ioombl1lem3  25552  ioombl1lem4  25553  addsqnreup  27431  addsval  27979  mulsval  28126  om2noseqrdg  28321  brcgr  28994  opiedgfv  29101  fsuppcurry1  32823  erlbrd  33351  rlocaddval  33356  rlocmulval  33357  fracerl  33397  sategoelfvb  35654  prv1n  35666  fvtransport  36267  bj-finsumval0  37652  poimirlem17  38011  poimirlem24  38018  poimirlem27  38021  dvhopvadd  41592  dvhopvsca  41601  dvhopaddN  41613  dvhopspN  41614  etransclem44  46728  gpgedgiov  48563  gpgedg2ov  48564  gpgedg2iv  48565  uspgrsprfo  48646  rngccoALTV  48769  ringccoALTV  48803  lmod1zr  48991  func2nd  49575  oppf1st2nd  49628  upfval3  49675  swapf2fval  49762  fucofval  49816  fuco112  49826  fuco21  49833  prcofvala  49874  lanfval  50110  ranfval  50111