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

Theorem op2ndg 7405
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 4588 . . 3 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
21fveqeq2d 6410 . 2 (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3 opeq2 4589 . . . 4 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
43fveq2d 6406 . . 3 (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5 id 22 . . 3 (𝑦 = 𝐵𝑦 = 𝐵)
64, 5eqeq12d 2817 . 2 (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7 vex 3390 . . 3 𝑥 ∈ V
8 vex 3390 . . 3 𝑦 ∈ V
97, 8op2nd 7401 . 2 (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
102, 6, 9vtocl2g 3459 1 ((𝐴𝑉𝐵𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2155  cop 4370  cfv 6095  2nd c2nd 7391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-sbc 3628  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-br 4838  df-opab 4900  df-mpt 4917  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-iota 6058  df-fun 6097  df-fv 6103  df-2nd 7393
This theorem is referenced by:  ot2ndg  7407  ot3rdg  7408  br2ndeqg  7415  2ndconst  7494  mpt2sn  7496  curry1  7497  xpmapenlem  8360  2ndinl  9031  2ndinr  9033  axdc4lem  9556  pinq  10028  addpipq  10038  mulpipq  10041  ordpipq  10043  swrdval  13634  ruclem1  15174  eucalg  15513  qnumdenbi  15663  setsstruct  16103  comffval  16557  oppccofval  16574  funcf2  16726  cofuval2  16745  resfval2  16751  resf2nd  16753  funcres  16754  isnat  16805  fucco  16820  homacd  16889  setcco  16931  catcco  16949  estrcco  16968  xpcco  17022  xpchom2  17025  xpcco2  17026  evlf2  17057  curfval  17062  curf1cl  17067  uncf1  17075  uncf2  17076  hof2fval  17094  yonedalem21  17112  yonedalem22  17117  mvmulfval  20553  imasdsf1olem  22385  ovolicc1  23491  ioombl1lem3  23535  ioombl1lem4  23536  brcgr  25988  opiedgfv  26095  fvtransport  32454  bj-elid3  33397  bj-finsumval0  33458  poimirlem17  33733  poimirlem24  33740  poimirlem27  33743  dvhopvadd  36868  dvhopvsca  36877  dvhopaddN  36889  dvhopspN  36890  etransclem44  40968  uspgrsprfo  42318  rngccoALTV  42550  ringccoALTV  42613  lmod1zr  42844
  Copyright terms: Public domain W3C validator