Theorem op2ndg 7939

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 4835	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6855	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4836	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6851	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2747	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3450	. . 3 ⊢ 𝑥 ∈ V
8		vex 3450	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7935	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3532	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ⟨cop 4597  ‘cfv 6501  2^nd c2nd 7925

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6453  df-fun 6503  df-fv 6509  df-2nd 7927

This theorem is referenced by:  ot2ndg  7941  ot3rdg  7942  br2ndeqg  7949  2ndconst  8038  mposn  8040  curry1  8041  opco2  8061  xpmapenlem  9095  2ndinl  9873  2ndinr  9875  axdc4lem  10400  pinq  10872  addpipq  10882  mulpipq  10885  ordpipq  10887  swrdval  14543  ruclem1  16124  eucalg  16474  qnumdenbi  16630  setsstruct  17059  comffval  17593  oppccofval  17611  funcf2  17768  cofuval2  17787  resfval2  17793  resf2nd  17795  funcres  17796  isnat  17848  fucco  17865  homacd  17941  setcco  17983  catcco  18005  estrcco  18031  xpcco  18085  xpchom2  18088  xpcco2  18089  evlf2  18121  curfval  18126  curf1cl  18131  uncf1  18139  uncf2  18140  hof2fval  18158  yonedalem21  18176  yonedalem22  18181  mvmulfval  21928  imasdsf1olem  23763  ovolicc1  24917  ioombl1lem3  24961  ioombl1lem4  24962  addsqnreup  26828  addsval  27317  mulsval  27417  brcgr  27912  opiedgfv  28021  fsuppcurry1  31710  sategoelfvb  34100  prv1n  34112  fvtransport  34693  bj-finsumval0  35829  poimirlem17  36168  poimirlem24  36175  poimirlem27  36178  dvhopvadd  39629  dvhopvsca  39638  dvhopaddN  39650  dvhopspN  39651  etransclem44  44639  uspgrsprfo  46170  rngccoALTV  46406  ringccoALTV  46469  lmod1zr  46694