Theorem op2ndg 7948

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4574  ‘cfv 6492  2^nd c2nd 7934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-2nd 7936

This theorem is referenced by:  ot2ndg  7950  ot3rdg  7951  br2ndeqg  7958  2ndconst  8044  mposn  8046  curry1  8047  opco2  8067  xpmapenlem  9075  2ndinl  9843  2ndinr  9845  axdc4lem  10368  pinq  10841  addpipq  10851  mulpipq  10854  ordpipq  10856  swrdval  14597  ruclem1  16189  eucalg  16547  qnumdenbi  16705  setsstruct  17137  comffval  17656  oppccofval  17673  funcf2  17826  cofuval2  17845  resfval2  17851  resf2nd  17853  funcres  17854  isnat  17908  fucco  17923  homacd  17999  setcco  18041  catcco  18063  estrcco  18087  xpcco  18140  xpchom2  18143  xpcco2  18144  evlf2  18175  curfval  18180  curf1cl  18185  uncf1  18193  uncf2  18194  hof2fval  18212  yonedalem21  18230  yonedalem22  18235  mvmulfval  22517  imasdsf1olem  24348  ovolicc1  25493  ioombl1lem3  25537  ioombl1lem4  25538  addsqnreup  27420  addsval  27968  mulsval  28115  om2noseqrdg  28310  brcgr  28983  opiedgfv  29090  fsuppcurry1  32812  erlbrd  33339  rlocaddval  33344  rlocmulval  33345  fracerl  33382  sategoelfvb  35617  prv1n  35629  fvtransport  36230  bj-finsumval0  37615  poimirlem17  37972  poimirlem24  37979  poimirlem27  37982  dvhopvadd  41553  dvhopvsca  41562  dvhopaddN  41574  dvhopspN  41575  etransclem44  46724  gpgedgiov  48553  gpgedg2ov  48554  gpgedg2iv  48555  uspgrsprfo  48636  rngccoALTV  48759  ringccoALTV  48793  lmod1zr  48981  func2nd  49565  oppf1st2nd  49618  upfval3  49665  swapf2fval  49752  fucofval  49806  fuco112  49816  fuco21  49823  prcofvala  49864  lanfval  50100  ranfval  50101