Theorem op2ndg 7984

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 4840	. . 3 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveqeq2d 6869	. 2 ⊢ (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3		opeq2 4841	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
4	3	fveq2d 6865	. . 3 ⊢ (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5		id 22	. . 3 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
6	4, 5	eqeq12d 2746	. 2 ⊢ (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7		vex 3454	. . 3 ⊢ 𝑥 ∈ V
8		vex 3454	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op2nd 7980	. 2 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
10	2, 6, 9	vtocl2g 3543	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4598  ‘cfv 6514  2^nd c2nd 7970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-2nd 7972

This theorem is referenced by:  ot2ndg  7986  ot3rdg  7987  br2ndeqg  7994  2ndconst  8083  mposn  8085  curry1  8086  opco2  8106  xpmapenlem  9114  2ndinl  9888  2ndinr  9890  axdc4lem  10415  pinq  10887  addpipq  10897  mulpipq  10900  ordpipq  10902  swrdval  14615  ruclem1  16206  eucalg  16564  qnumdenbi  16721  setsstruct  17153  comffval  17667  oppccofval  17684  funcf2  17837  cofuval2  17856  resfval2  17862  resf2nd  17864  funcres  17865  isnat  17919  fucco  17934  homacd  18010  setcco  18052  catcco  18074  estrcco  18098  xpcco  18151  xpchom2  18154  xpcco2  18155  evlf2  18186  curfval  18191  curf1cl  18196  uncf1  18204  uncf2  18205  hof2fval  18223  yonedalem21  18241  yonedalem22  18246  mvmulfval  22436  imasdsf1olem  24268  ovolicc1  25424  ioombl1lem3  25468  ioombl1lem4  25469  addsqnreup  27361  addsval  27876  mulsval  28019  om2noseqrdg  28205  brcgr  28834  opiedgfv  28941  fsuppcurry1  32655  erlbrd  33221  rlocaddval  33226  rlocmulval  33227  fracerl  33263  sategoelfvb  35413  prv1n  35425  fvtransport  36027  bj-finsumval0  37280  poimirlem17  37638  poimirlem24  37645  poimirlem27  37648  dvhopvadd  41094  dvhopvsca  41103  dvhopaddN  41115  dvhopspN  41116  etransclem44  46283  gpgedgiov  48060  gpgedg2ov  48061  gpgedg2iv  48062  uspgrsprfo  48140  rngccoALTV  48263  ringccoALTV  48297  lmod1zr  48486  func2nd  49071  oppf1st2nd  49124  upfval3  49171  swapf2fval  49258  fucofval  49312  fuco112  49322  fuco21  49329  prcofvala  49370  lanfval  49606  ranfval  49607