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 4834	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6879	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4835	. . . 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 5251  ax-nul 5261  ax-pr 5395  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 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  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  14671  ruclem1  16277  eucalg  16635  qnumdenbi  16793  setsstruct  17226  comffval  17745  oppccofval  17762  funcf2  17915  cofuval2  17934  resfval2  17940  resf2nd  17942  funcres  17943  isnat  17997  fucco  18012  homacd  18088  setcco  18130  catcco  18152  estrcco  18176  xpcco  18229  xpchom2  18232  xpcco2  18233  evlf2  18264  curfval  18269  curf1cl  18274  uncf1  18282  uncf2  18283  hof2fval  18301  yonedalem21  18319  yonedalem22  18324  mvmulfval  22660  imasdsf1olem  24491  ovolicc1  25636  ioombl1lem3  25680  ioombl1lem4  25681  addsqnreup  27565  addsval  28113  mulsval  28260  om2noseqrdg  28455  brcgr  29159  opiedgfv  29266  fsuppcurry1  32981  erlbrd  33496  erld2  33499  rlocaddval  33502  rlocmulval  33503  fracerl  33542  sategoelfvb  35782  prv1n  35794  fvtransport  36395  bj-finsumval0  37789  poimirlem17  38148  poimirlem24  38155  poimirlem27  38158  dvhopvadd  41729  dvhopvsca  41738  dvhopaddN  41750  dvhopspN  41751  etransclem44  46850  gpgedgiov  48685  gpgedg2ov  48686  gpgedg2iv  48687  uspgrsprfo  48768  rngccoALTV  48891  ringccoALTV  48925  lmod1zr  49124  func2nd  49707  oppf1st2nd  49760  upfval3  49807  swapf2fval  49894  fucofval  49948  fuco112  49958  fuco21  49965  prcofvala  50006  lanfval  50242  ranfval  50243