Theorem op2ndg 7516

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 4678	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6509	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4679	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6505	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2793	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3418	. . 3 ⊢ 𝑥 ∈ V
8		vex 3418	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7512	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3490	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2050  ⟨cop 4448  ‘cfv 6190  2^nd c2nd 7502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-iota 6154  df-fun 6192  df-fv 6198  df-2nd 7504

This theorem is referenced by:  ot2ndg  7518  ot3rdg  7519  br2ndeqg  7526  2ndconst  7606  mposn  7608  curry1  7609  xpmapenlem  8482  2ndinl  9153  2ndinr  9155  axdc4lem  9677  pinq  10149  addpipq  10159  mulpipq  10162  ordpipq  10164  swrdval  13809  ruclem1  15447  eucalg  15790  qnumdenbi  15943  setsstruct  16382  comffval  16830  oppccofval  16847  funcf2  16999  cofuval2  17018  resfval2  17024  resf2nd  17026  funcres  17027  isnat  17078  fucco  17093  homacd  17162  setcco  17204  catcco  17222  estrcco  17241  xpcco  17294  xpchom2  17297  xpcco2  17298  evlf2  17329  curfval  17334  curf1cl  17339  uncf1  17347  uncf2  17348  hof2fval  17366  yonedalem21  17384  yonedalem22  17389  mvmulfval  20858  imasdsf1olem  22689  ovolicc1  23823  ioombl1lem3  23867  ioombl1lem4  23868  addsqnreup  25724  brcgr  26392  opiedgfv  26498  fsuppcurry1  30216  fvtransport  33014  bj-elid3  33940  bj-finsumval0  34030  poimirlem17  34350  poimirlem24  34357  poimirlem27  34360  dvhopvadd  37674  dvhopvsca  37683  dvhopaddN  37695  dvhopspN  37696  etransclem44  41995  uspgrsprfo  43392  rngccoALTV  43624  ringccoALTV  43687  lmod1zr  43916