MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  op2ndg Structured version   Visualization version   GIF version

Theorem op2ndg 7931
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.
StepHypRef Expression
1 opeq1 4829 . . 3 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
21fveqeq2d 6848 . 2 (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3 opeq2 4830 . . . 4 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
43fveq2d 6844 . . 3 (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5 id 22 . . 3 (𝑦 = 𝐵𝑦 = 𝐵)
64, 5eqeq12d 2752 . 2 (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7 vex 3448 . . 3 𝑥 ∈ V
8 vex 3448 . . 3 𝑦 ∈ V
97, 8op2nd 7927 . 2 (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
102, 6, 9vtocl2g 3530 1 ((𝐴𝑉𝐵𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  cop 4591  cfv 6494  2nd c2nd 7917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5255  ax-nul 5262  ax-pr 5383  ax-un 7669
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5530  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6446  df-fun 6496  df-fv 6502  df-2nd 7919
This theorem is referenced by:  ot2ndg  7933  ot3rdg  7934  br2ndeqg  7941  2ndconst  8030  mposn  8032  curry1  8033  opco2  8053  xpmapenlem  9085  2ndinl  9861  2ndinr  9863  axdc4lem  10388  pinq  10860  addpipq  10870  mulpipq  10873  ordpipq  10875  swrdval  14528  ruclem1  16110  eucalg  16460  qnumdenbi  16616  setsstruct  17045  comffval  17576  oppccofval  17594  funcf2  17751  cofuval2  17770  resfval2  17776  resf2nd  17778  funcres  17779  isnat  17831  fucco  17848  homacd  17924  setcco  17966  catcco  17988  estrcco  18014  xpcco  18068  xpchom2  18071  xpcco2  18072  evlf2  18104  curfval  18109  curf1cl  18114  uncf1  18122  uncf2  18123  hof2fval  18141  yonedalem21  18159  yonedalem22  18164  mvmulfval  21887  imasdsf1olem  23722  ovolicc1  24876  ioombl1lem3  24920  ioombl1lem4  24921  addsqnreup  26787  brcgr  27747  opiedgfv  27856  fsuppcurry1  31537  sategoelfvb  33904  prv1n  33916  addsval  34300  mulsval  34397  fvtransport  34606  bj-finsumval0  35745  poimirlem17  36084  poimirlem24  36091  poimirlem27  36094  dvhopvadd  39545  dvhopvsca  39554  dvhopaddN  39566  dvhopspN  39567  etransclem44  44489  uspgrsprfo  46020  rngccoALTV  46256  ringccoALTV  46319  lmod1zr  46544
  Copyright terms: Public domain W3C validator