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

Theorem op2ndg 7935
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 4831 . . 3 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
21fveqeq2d 6851 . 2 (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3 opeq2 4832 . . . 4 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
43fveq2d 6847 . . 3 (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5 id 22 . . 3 (𝑦 = 𝐵𝑦 = 𝐵)
64, 5eqeq12d 2753 . 2 (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7 vex 3450 . . 3 𝑥 ∈ V
8 vex 3450 . . 3 𝑦 ∈ V
97, 8op2nd 7931 . 2 (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
102, 6, 9vtocl2g 3532 1 ((𝐴𝑉𝐵𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  cop 4593  cfv 6497  2nd c2nd 7921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fv 6505  df-2nd 7923
This theorem is referenced by:  ot2ndg  7937  ot3rdg  7938  br2ndeqg  7945  2ndconst  8034  mposn  8036  curry1  8037  opco2  8057  xpmapenlem  9089  2ndinl  9865  2ndinr  9867  axdc4lem  10392  pinq  10864  addpipq  10874  mulpipq  10877  ordpipq  10879  swrdval  14532  ruclem1  16114  eucalg  16464  qnumdenbi  16620  setsstruct  17049  comffval  17580  oppccofval  17598  funcf2  17755  cofuval2  17774  resfval2  17780  resf2nd  17782  funcres  17783  isnat  17835  fucco  17852  homacd  17928  setcco  17970  catcco  17992  estrcco  18018  xpcco  18072  xpchom2  18075  xpcco2  18076  evlf2  18108  curfval  18113  curf1cl  18118  uncf1  18126  uncf2  18127  hof2fval  18145  yonedalem21  18163  yonedalem22  18168  mvmulfval  21894  imasdsf1olem  23729  ovolicc1  24883  ioombl1lem3  24927  ioombl1lem4  24928  addsqnreup  26794  addsval  27277  brcgr  27852  opiedgfv  27961  fsuppcurry1  31645  sategoelfvb  34016  prv1n  34028  mulsval  34411  fvtransport  34620  bj-finsumval0  35759  poimirlem17  36098  poimirlem24  36105  poimirlem27  36108  dvhopvadd  39559  dvhopvsca  39568  dvhopaddN  39580  dvhopspN  39581  etransclem44  44526  uspgrsprfo  46057  rngccoALTV  46293  ringccoALTV  46356  lmod1zr  46581
  Copyright terms: Public domain W3C validator