Theorem op2ndg 7999

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 4849	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6883	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4850	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6879	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2751	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3463	. . 3 ⊢ 𝑥 ∈ V
8		vex 3463	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7995	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3553	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ⟨cop 4607  ‘cfv 6530  2^nd c2nd 7985

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fv 6538  df-2nd 7987

This theorem is referenced by:  ot2ndg  8001  ot3rdg  8002  br2ndeqg  8009  2ndconst  8098  mposn  8100  curry1  8101  opco2  8121  xpmapenlem  9156  2ndinl  9940  2ndinr  9942  axdc4lem  10467  pinq  10939  addpipq  10949  mulpipq  10952  ordpipq  10954  swrdval  14659  ruclem1  16247  eucalg  16604  qnumdenbi  16761  setsstruct  17193  comffval  17709  oppccofval  17726  funcf2  17879  cofuval2  17898  resfval2  17904  resf2nd  17906  funcres  17907  isnat  17961  fucco  17976  homacd  18052  setcco  18094  catcco  18116  estrcco  18140  xpcco  18193  xpchom2  18196  xpcco2  18197  evlf2  18228  curfval  18233  curf1cl  18238  uncf1  18246  uncf2  18247  hof2fval  18265  yonedalem21  18283  yonedalem22  18288  mvmulfval  22478  imasdsf1olem  24310  ovolicc1  25467  ioombl1lem3  25511  ioombl1lem4  25512  addsqnreup  27404  addsval  27912  mulsval  28052  om2noseqrdg  28227  brcgr  28825  opiedgfv  28932  fsuppcurry1  32648  erlbrd  33204  rlocaddval  33209  rlocmulval  33210  fracerl  33246  sategoelfvb  35387  prv1n  35399  fvtransport  35996  bj-finsumval0  37249  poimirlem17  37607  poimirlem24  37614  poimirlem27  37617  dvhopvadd  41058  dvhopvsca  41067  dvhopaddN  41079  dvhopspN  41080  etransclem44  46255  uspgrsprfo  48071  rngccoALTV  48194  ringccoALTV  48228  lmod1zr  48417  oppf1st2nd  49027  upfval3  49061  swapf2fval  49130  fucofval  49178  fuco112  49188  fuco21  49195  prcofvala  49236  lanfval  49438  ranfval  49439