Theorem op2ndg 8025

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ⟨cop 4636  ‘cfv 6562  2^nd c2nd 8011

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-2nd 8013

This theorem is referenced by:  ot2ndg  8027  ot3rdg  8028  br2ndeqg  8035  2ndconst  8124  mposn  8126  curry1  8127  opco2  8147  xpmapenlem  9182  2ndinl  9965  2ndinr  9967  axdc4lem  10492  pinq  10964  addpipq  10974  mulpipq  10977  ordpipq  10979  swrdval  14677  ruclem1  16263  eucalg  16620  qnumdenbi  16777  setsstruct  17209  comffval  17743  oppccofval  17761  funcf2  17918  cofuval2  17937  resfval2  17943  resf2nd  17945  funcres  17946  isnat  18001  fucco  18018  homacd  18094  setcco  18136  catcco  18158  estrcco  18184  xpcco  18238  xpchom2  18241  xpcco2  18242  evlf2  18274  curfval  18279  curf1cl  18284  uncf1  18292  uncf2  18293  hof2fval  18311  yonedalem21  18329  yonedalem22  18334  mvmulfval  22563  imasdsf1olem  24398  ovolicc1  25564  ioombl1lem3  25608  ioombl1lem4  25609  addsqnreup  27501  addsval  28009  mulsval  28149  om2noseqrdg  28324  brcgr  28929  opiedgfv  29038  fsuppcurry1  32742  erlbrd  33249  rlocaddval  33254  rlocmulval  33255  fracerl  33287  sategoelfvb  35403  prv1n  35415  fvtransport  36013  bj-finsumval0  37267  poimirlem17  37623  poimirlem24  37630  poimirlem27  37633  dvhopvadd  41075  dvhopvsca  41084  dvhopaddN  41096  dvhopspN  41097  etransclem44  46233  uspgrsprfo  47991  rngccoALTV  48114  ringccoALTV  48148  lmod1zr  48338