Theorem op2ndg 7934

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 4822	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6830	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4823	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6826	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2747	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3440	. . 3 ⊢ 𝑥 ∈ V
8		vex 3440	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7930	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3525	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ⟨cop 4579  ‘cfv 6481  2^nd c2nd 7920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6437  df-fun 6483  df-fv 6489  df-2nd 7922

This theorem is referenced by:  ot2ndg  7936  ot3rdg  7937  br2ndeqg  7944  2ndconst  8031  mposn  8033  curry1  8034  opco2  8054  xpmapenlem  9057  2ndinl  9821  2ndinr  9823  axdc4lem  10346  pinq  10818  addpipq  10828  mulpipq  10831  ordpipq  10833  swrdval  14551  ruclem1  16140  eucalg  16498  qnumdenbi  16655  setsstruct  17087  comffval  17605  oppccofval  17622  funcf2  17775  cofuval2  17794  resfval2  17800  resf2nd  17802  funcres  17803  isnat  17857  fucco  17872  homacd  17948  setcco  17990  catcco  18012  estrcco  18036  xpcco  18089  xpchom2  18092  xpcco2  18093  evlf2  18124  curfval  18129  curf1cl  18134  uncf1  18142  uncf2  18143  hof2fval  18161  yonedalem21  18179  yonedalem22  18184  mvmulfval  22457  imasdsf1olem  24288  ovolicc1  25444  ioombl1lem3  25488  ioombl1lem4  25489  addsqnreup  27381  addsval  27905  mulsval  28048  om2noseqrdg  28234  brcgr  28878  opiedgfv  28985  fsuppcurry1  32707  erlbrd  33230  rlocaddval  33235  rlocmulval  33236  fracerl  33272  sategoelfvb  35463  prv1n  35475  fvtransport  36076  bj-finsumval0  37329  poimirlem17  37676  poimirlem24  37683  poimirlem27  37686  dvhopvadd  41191  dvhopvsca  41200  dvhopaddN  41212  dvhopspN  41213  etransclem44  46375  gpgedgiov  48164  gpgedg2ov  48165  gpgedg2iv  48166  uspgrsprfo  48247  rngccoALTV  48370  ringccoALTV  48404  lmod1zr  48593  func2nd  49178  oppf1st2nd  49231  upfval3  49278  swapf2fval  49365  fucofval  49419  fuco112  49429  fuco21  49436  prcofvala  49477  lanfval  49713  ranfval  49714