Theorem op2ndg 8003

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 6885	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4834	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6881	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 23	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2777	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3455	. . 3 ⊢ 𝑥 ∈ V
8		vex 3455	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7999	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3534	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ⟨cop 4590  ‘cfv 6531  2^nd c2nd 7989

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fv 6539  df-2nd 7991

This theorem is used by:  ot2ndg  8005  ot3rdg  8006  br2ndeqg  8013  2ndconst  8101  mposn  8103  curry1  8104  opco2  8124  xpmapenlem  9147  2ndinl  9990  2ndinr  9992  axdc4lem  10514  pinq  10993  addpipq  11003  mulpipq  11006  ordpipq  11008  swrdval  14771  ruclem1  16379  eucalg  16742  qnumdenbi  16900  setsstruct  17334  comffval  17853  oppccofval  17870  funcf2  18023  cofuval2  18042  resfval2  18048  resf2nd  18050  funcres  18051  isnat  18105  fucco  18120  homacd  18196  setcco  18238  catcco  18260  estrcco  18284  xpcco  18337  xpchom2  18340  xpcco2  18341  evlf2  18372  curfval  18377  curf1cl  18382  uncf1  18390  uncf2  18391  hof2fval  18409  yonedalem21  18427  yonedalem22  18432  mvmulfval  22837  imasdsf1olem  24672  ovolicc1  25817  ioombl1lem3  25861  ioombl1lem4  25862  addsqnreup  27752  addsval  28330  mulsval  28477  om2noseqrdg  28672  brcgr  29460  opiedgfv  29567  fsuppcurry1  33298  erlbrd  33806  erld2  33809  rlocaddval  33812  rlocmulval  33813  fracerl  33850  sategoelfvb  36153  prv1n  36165  fvtransport  36767  bj-finsumval0  38174  poimirlem17  38523  poimirlem24  38530  poimirlem27  38533  dvhopvadd  42118  dvhopvsca  42127  dvhopaddN  42139  dvhopspN  42140  etransclem44  47232  gpgedgiov  49107  gpgedg2ov  49108  gpgedg2iv  49109  uspgrsprfo  49190  rngccoALTV  49312  ringccoALTV  49346  lmod1zr  49549  func2nd  50130  oppf1st2nd  50183  upfval3  50230  swapf2fval  50317  fucofval  50371  fuco112  50381  fuco21  50388  prcofvala  50429  lanfval  50665  ranfval  50666