Theorem op2ndg 7979

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 4830	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6871	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4831	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6867	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2777	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3457	. . 3 ⊢ 𝑥 ∈ V
8		vex 3457	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7975	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3538	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ⟨cop 4587  ‘cfv 6517  2^nd c2nd 7965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fv 6525  df-2nd 7967

This theorem is referenced by:  ot2ndg  7981  ot3rdg  7982  br2ndeqg  7989  2ndconst  8075  mposn  8077  curry1  8078  opco2  8098  xpmapenlem  9112  2ndinl  9883  2ndinr  9885  axdc4lem  10409  pinq  10882  addpipq  10892  mulpipq  10895  ordpipq  10897  swrdval  14654  ruclem1  16246  eucalg  16604  qnumdenbi  16762  setsstruct  17195  comffval  17714  oppccofval  17731  funcf2  17884  cofuval2  17903  resfval2  17909  resf2nd  17911  funcres  17912  isnat  17966  fucco  17981  homacd  18057  setcco  18099  catcco  18121  estrcco  18145  xpcco  18198  xpchom2  18201  xpcco2  18202  evlf2  18233  curfval  18238  curf1cl  18243  uncf1  18251  uncf2  18252  hof2fval  18270  yonedalem21  18288  yonedalem22  18293  mvmulfval  22582  imasdsf1olem  24413  ovolicc1  25558  ioombl1lem3  25602  ioombl1lem4  25603  addsqnreup  27484  addsval  28032  mulsval  28179  om2noseqrdg  28374  brcgr  29047  opiedgfv  29154  fsuppcurry1  32876  erlbrd  33405  erld2  33408  rlocaddval  33411  rlocmulval  33412  fracerl  33454  sategoelfvb  35733  prv1n  35745  fvtransport  36346  bj-finsumval0  37741  poimirlem17  38100  poimirlem24  38107  poimirlem27  38110  dvhopvadd  41681  dvhopvsca  41690  dvhopaddN  41702  dvhopspN  41703  etransclem44  46816  gpgedgiov  48651  gpgedg2ov  48652  gpgedg2iv  48653  uspgrsprfo  48734  rngccoALTV  48857  ringccoALTV  48891  lmod1zr  49079  func2nd  49663  oppf1st2nd  49716  upfval3  49763  swapf2fval  49850  fucofval  49904  fuco112  49914  fuco21  49921  prcofvala  49962  lanfval  50198  ranfval  50199