Theorem op2ndg 7981

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 4837	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6866	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4838	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6862	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2745	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3451	. . 3 ⊢ 𝑥 ∈ V
8		vex 3451	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7977	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3540	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4595  ‘cfv 6511  2^nd c2nd 7967

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fv 6519  df-2nd 7969

This theorem is referenced by:  ot2ndg  7983  ot3rdg  7984  br2ndeqg  7991  2ndconst  8080  mposn  8082  curry1  8083  opco2  8103  xpmapenlem  9108  2ndinl  9881  2ndinr  9883  axdc4lem  10408  pinq  10880  addpipq  10890  mulpipq  10893  ordpipq  10895  swrdval  14608  ruclem1  16199  eucalg  16557  qnumdenbi  16714  setsstruct  17146  comffval  17660  oppccofval  17677  funcf2  17830  cofuval2  17849  resfval2  17855  resf2nd  17857  funcres  17858  isnat  17912  fucco  17927  homacd  18003  setcco  18045  catcco  18067  estrcco  18091  xpcco  18144  xpchom2  18147  xpcco2  18148  evlf2  18179  curfval  18184  curf1cl  18189  uncf1  18197  uncf2  18198  hof2fval  18216  yonedalem21  18234  yonedalem22  18239  mvmulfval  22429  imasdsf1olem  24261  ovolicc1  25417  ioombl1lem3  25461  ioombl1lem4  25462  addsqnreup  27354  addsval  27869  mulsval  28012  om2noseqrdg  28198  brcgr  28827  opiedgfv  28934  fsuppcurry1  32648  erlbrd  33214  rlocaddval  33219  rlocmulval  33220  fracerl  33256  sategoelfvb  35406  prv1n  35418  fvtransport  36020  bj-finsumval0  37273  poimirlem17  37631  poimirlem24  37638  poimirlem27  37641  dvhopvadd  41087  dvhopvsca  41096  dvhopaddN  41108  dvhopspN  41109  etransclem44  46276  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  uspgrsprfo  48136  rngccoALTV  48259  ringccoALTV  48293  lmod1zr  48482  func2nd  49067  oppf1st2nd  49120  upfval3  49167  swapf2fval  49254  fucofval  49308  fuco112  49318  fuco21  49325  prcofvala  49366  lanfval  49602  ranfval  49603