MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  op2nd Structured version   Unicode version

Theorem op2nd 6708
Description: Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
Hypotheses
Ref Expression
op1st.1  |-  A  e. 
_V
op1st.2  |-  B  e. 
_V
Assertion
Ref Expression
op2nd  |-  ( 2nd `  <. A ,  B >. )  =  B

Proof of Theorem op2nd
StepHypRef Expression
1 2ndval 6702 . 2  |-  ( 2nd `  <. A ,  B >. )  =  U. ran  {
<. A ,  B >. }
2 op1st.1 . . 3  |-  A  e. 
_V
3 op1st.2 . . 3  |-  B  e. 
_V
42, 3op2nda 5401 . 2  |-  U. ran  {
<. A ,  B >. }  =  B
51, 4eqtri 2411 1  |-  ( 2nd `  <. A ,  B >. )  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1399    e. wcel 1826   _Vcvv 3034   {csn 3944   <.cop 3950   U.cuni 4163   ran crn 4914   ` cfv 5496   2ndc2nd 6698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-iota 5460  df-fun 5498  df-fv 5504  df-2nd 6700
This theorem is referenced by:  op2ndd  6710  op2ndg  6712  2ndval2  6717  fo2ndres  6724  eloprabi  6761  fo2ndf  6806  f1o2ndf1  6807  seqomlem1  7033  seqomlem2  7034  xpmapenlem  7603  fseqenlem2  8319  axdc4lem  8748  iunfo  8827  archnq  9269  om2uzrdg  11970  uzrdgsuci  11974  fsum2dlem  13587  fprod2dlem  13786  ruclem8  13972  ruclem11  13975  eucalglt  14216  idfu2nd  15283  idfucl  15287  cofu2nd  15291  cofucl  15294  xpccatid  15574  prf2nd  15591  curf2ndf  15633  yonedalem22  15664  gaid  16454  2ndcctbss  20041  upxp  20209  uptx  20211  txkgen  20238  cnheiborlem  21539  ovollb2lem  21984  ovolctb  21986  ovoliunlem2  21999  ovolshftlem1  22005  ovolscalem1  22009  ovolicc1  22012  wlknwwlknsur  24833  wlkiswwlksur  24840  clwlkfoclwwlk  24966  ex-2nd  25287  cnnvs  25703  cnnvnm  25704  h2hsm  26009  h2hnm  26010  hhsssm  26293  hhssnm  26294  aciunf1lem  27648  eulerpartlemgvv  28498  eulerpartlemgh  28500  msubff1  29105  msubvrs  29109  br2ndeq  29370  heiborlem7  30479  heiborlem8  30480  pellexlem5  30934  pellex  30936  dvnprodlem1  31909  dvhvaddass  37237  dvhlveclem  37248  diblss  37310
  Copyright terms: Public domain W3C validator