Theorem op2ndg 7944

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 4827	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6834	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4828	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6830	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2745	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3442	. . 3 ⊢ 𝑥 ∈ V
8		vex 3442	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7940	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3531	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4585  ‘cfv 6486  2^nd c2nd 7930

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 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6442  df-fun 6488  df-fv 6494  df-2nd 7932

This theorem is referenced by:  ot2ndg  7946  ot3rdg  7947  br2ndeqg  7954  2ndconst  8041  mposn  8043  curry1  8044  opco2  8064  xpmapenlem  9068  2ndinl  9843  2ndinr  9845  axdc4lem  10368  pinq  10840  addpipq  10850  mulpipq  10853  ordpipq  10855  swrdval  14568  ruclem1  16158  eucalg  16516  qnumdenbi  16673  setsstruct  17105  comffval  17623  oppccofval  17640  funcf2  17793  cofuval2  17812  resfval2  17818  resf2nd  17820  funcres  17821  isnat  17875  fucco  17890  homacd  17966  setcco  18008  catcco  18030  estrcco  18054  xpcco  18107  xpchom2  18110  xpcco2  18111  evlf2  18142  curfval  18147  curf1cl  18152  uncf1  18160  uncf2  18161  hof2fval  18179  yonedalem21  18197  yonedalem22  18202  mvmulfval  22445  imasdsf1olem  24277  ovolicc1  25433  ioombl1lem3  25477  ioombl1lem4  25478  addsqnreup  27370  addsval  27892  mulsval  28035  om2noseqrdg  28221  brcgr  28863  opiedgfv  28970  fsuppcurry1  32681  erlbrd  33213  rlocaddval  33218  rlocmulval  33219  fracerl  33255  sategoelfvb  35391  prv1n  35403  fvtransport  36005  bj-finsumval0  37258  poimirlem17  37616  poimirlem24  37623  poimirlem27  37626  dvhopvadd  41072  dvhopvsca  41081  dvhopaddN  41093  dvhopspN  41094  etransclem44  46260  gpgedgiov  48050  gpgedg2ov  48051  gpgedg2iv  48052  uspgrsprfo  48133  rngccoALTV  48256  ringccoALTV  48290  lmod1zr  48479  func2nd  49064  oppf1st2nd  49117  upfval3  49164  swapf2fval  49251  fucofval  49305  fuco112  49315  fuco21  49322  prcofvala  49363  lanfval  49599  ranfval  49600