Theorem op2ndg 7987

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 4833	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6879	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4834	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6875	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 23	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2781	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3461	. . 3 ⊢ 𝑥 ∈ V
8		vex 3461	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7983	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3541	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ⟨cop 4591  ‘cfv 6525  2^nd c2nd 7973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6481  df-fun 6527  df-fv 6533  df-2nd 7975

This theorem is referenced by:  ot2ndg  7989  ot3rdg  7990  br2ndeqg  7997  2ndconst  8084  mposn  8086  curry1  8087  opco2  8107  xpmapenlem  9120  2ndinl  9902  2ndinr  9904  axdc4lem  10427  pinq  10900  addpipq  10910  mulpipq  10913  ordpipq  10915  swrdval  14669  ruclem1  16275  eucalg  16633  qnumdenbi  16791  setsstruct  17224  comffval  17743  oppccofval  17760  funcf2  17913  cofuval2  17932  resfval2  17938  resf2nd  17940  funcres  17941  isnat  17995  fucco  18010  homacd  18086  setcco  18128  catcco  18150  estrcco  18174  xpcco  18227  xpchom2  18230  xpcco2  18231  evlf2  18262  curfval  18267  curf1cl  18272  uncf1  18280  uncf2  18281  hof2fval  18299  yonedalem21  18317  yonedalem22  18322  mvmulfval  22656  imasdsf1olem  24487  ovolicc1  25632  ioombl1lem3  25676  ioombl1lem4  25677  addsqnreup  27561  addsval  28109  mulsval  28256  om2noseqrdg  28451  brcgr  29155  opiedgfv  29262  fsuppcurry1  32977  erlbrd  33491  erld2  33494  rlocaddval  33497  rlocmulval  33498  fracerl  33537  sategoelfvb  35777  prv1n  35789  fvtransport  36390  bj-finsumval0  37784  poimirlem17  38143  poimirlem24  38150  poimirlem27  38153  dvhopvadd  41724  dvhopvsca  41733  dvhopaddN  41745  dvhopspN  41746  etransclem44  46851  gpgedgiov  48686  gpgedg2ov  48687  gpgedg2iv  48688  uspgrsprfo  48769  rngccoALTV  48892  ringccoALTV  48926  lmod1zr  49125  func2nd  49708  oppf1st2nd  49761  upfval3  49808  swapf2fval  49895  fucofval  49949  fuco112  49959  fuco21  49966  prcofvala  50007  lanfval  50243  ranfval  50244