Theorem op2ndg 7956

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 4831	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6850	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4832	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6846	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2753	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3446	. . 3 ⊢ 𝑥 ∈ V
8		vex 3446	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7952	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3531	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4588  ‘cfv 6500  2^nd c2nd 7942

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fv 6508  df-2nd 7944

This theorem is referenced by:  ot2ndg  7958  ot3rdg  7959  br2ndeqg  7966  2ndconst  8053  mposn  8055  curry1  8056  opco2  8076  xpmapenlem  9084  2ndinl  9852  2ndinr  9854  axdc4lem  10377  pinq  10850  addpipq  10860  mulpipq  10863  ordpipq  10865  swrdval  14579  ruclem1  16168  eucalg  16526  qnumdenbi  16683  setsstruct  17115  comffval  17634  oppccofval  17651  funcf2  17804  cofuval2  17823  resfval2  17829  resf2nd  17831  funcres  17832  isnat  17886  fucco  17901  homacd  17977  setcco  18019  catcco  18041  estrcco  18065  xpcco  18118  xpchom2  18121  xpcco2  18122  evlf2  18153  curfval  18158  curf1cl  18163  uncf1  18171  uncf2  18172  hof2fval  18190  yonedalem21  18208  yonedalem22  18213  mvmulfval  22498  imasdsf1olem  24329  ovolicc1  25485  ioombl1lem3  25529  ioombl1lem4  25530  addsqnreup  27422  addsval  27970  mulsval  28117  om2noseqrdg  28312  brcgr  28985  opiedgfv  29092  fsuppcurry1  32813  erlbrd  33356  rlocaddval  33361  rlocmulval  33362  fracerl  33399  sategoelfvb  35632  prv1n  35644  fvtransport  36245  bj-finsumval0  37534  poimirlem17  37882  poimirlem24  37889  poimirlem27  37892  dvhopvadd  41463  dvhopvsca  41472  dvhopaddN  41484  dvhopspN  41485  etransclem44  46630  gpgedgiov  48419  gpgedg2ov  48420  gpgedg2iv  48421  uspgrsprfo  48502  rngccoALTV  48625  ringccoALTV  48659  lmod1zr  48847  func2nd  49431  oppf1st2nd  49484  upfval3  49531  swapf2fval  49618  fucofval  49672  fuco112  49682  fuco21  49689  prcofvala  49730  lanfval  49966  ranfval  49967