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

Theorem op2ndg 7688
 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 4766 . . 3 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
21fveqeq2d 6657 . 2 (𝑥 = 𝐴 → ((2nd ‘⟨𝑥, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝑦⟩) = 𝑦))
3 opeq2 4768 . . . 4 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
43fveq2d 6653 . . 3 (𝑦 = 𝐵 → (2nd ‘⟨𝐴, 𝑦⟩) = (2nd ‘⟨𝐴, 𝐵⟩))
5 id 22 . . 3 (𝑦 = 𝐵𝑦 = 𝐵)
64, 5eqeq12d 2817 . 2 (𝑦 = 𝐵 → ((2nd ‘⟨𝐴, 𝑦⟩) = 𝑦 ↔ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵))
7 vex 3447 . . 3 𝑥 ∈ V
8 vex 3447 . . 3 𝑦 ∈ V
97, 8op2nd 7684 . 2 (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
102, 6, 9vtocl2g 3523 1 ((𝐴𝑉𝐵𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2112  ⟨cop 4534  ‘cfv 6328  2nd c2nd 7674 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-iota 6287  df-fun 6330  df-fv 6336  df-2nd 7676 This theorem is referenced by:  ot2ndg  7690  ot3rdg  7691  br2ndeqg  7698  2ndconst  7783  mposn  7785  curry1  7786  xpmapenlem  8672  2ndinl  9345  2ndinr  9347  axdc4lem  9870  pinq  10342  addpipq  10352  mulpipq  10355  ordpipq  10357  swrdval  14000  ruclem1  15580  eucalg  15925  qnumdenbi  16078  setsstruct  16519  comffval  16965  oppccofval  16982  funcf2  17134  cofuval2  17153  resfval2  17159  resf2nd  17161  funcres  17162  isnat  17213  fucco  17228  homacd  17297  setcco  17339  catcco  17357  estrcco  17376  xpcco  17429  xpchom2  17432  xpcco2  17433  evlf2  17464  curfval  17469  curf1cl  17474  uncf1  17482  uncf2  17483  hof2fval  17501  yonedalem21  17519  yonedalem22  17524  mvmulfval  21151  imasdsf1olem  22984  ovolicc1  24124  ioombl1lem3  24168  ioombl1lem4  24169  addsqnreup  26031  brcgr  26698  opiedgfv  26804  fsuppcurry1  30491  sategoelfvb  32780  prv1n  32792  fvtransport  33607  bj-finsumval0  34701  poimirlem17  35073  poimirlem24  35080  poimirlem27  35083  dvhopvadd  38388  dvhopvsca  38397  dvhopaddN  38409  dvhopspN  38410  etransclem44  42917  uspgrsprfo  44373  rngccoALTV  44609  ringccoALTV  44672  lmod1zr  44899
 Copyright terms: Public domain W3C validator