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

Theorem op2nd 6575
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 6569 . 2  |-  ( 2nd `  <. A ,  B >. )  =  U. ran  {
<. A ,  B >. }
2 op1st.1 . . 3  |-  A  e. 
_V
3 op1st.2 . . 3  |-  B  e. 
_V
42, 3op2nda 5312 . 2  |-  U. ran  {
<. A ,  B >. }  =  B
51, 4eqtri 2453 1  |-  ( 2nd `  <. A ,  B >. )  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    e. wcel 1755   _Vcvv 2962   {csn 3865   <.cop 3871   U.cuni 4079   ran crn 4828   ` cfv 5406   2ndc2nd 6565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-iota 5369  df-fun 5408  df-fv 5414  df-2nd 6567
This theorem is referenced by:  op2ndd  6577  op2ndg  6579  2ndval2  6584  fo2ndres  6590  eloprabi  6625  fo2ndf  6668  f1o2ndf1  6669  seqomlem1  6891  seqomlem2  6892  xpmapenlem  7466  fseqenlem2  8183  axdc4lem  8612  iunfo  8691  archnq  9136  om2uzrdg  11762  uzrdgsuci  11766  fsum2dlem  13220  ruclem8  13501  ruclem11  13504  eucalglt  13742  idfu2nd  14769  idfucl  14773  cofu2nd  14777  cofucl  14780  xpccatid  14980  prf2nd  14997  curf2ndf  15039  yonedalem22  15070  gaid  15796  2ndcctbss  18900  upxp  19037  uptx  19039  txkgen  19066  cnheiborlem  20367  ovollb2lem  20812  ovolctb  20814  ovoliunlem2  20827  ovolshftlem1  20833  ovolscalem1  20837  ovolicc1  20840  ex-2nd  23474  cnnvs  23893  cnnvnm  23894  h2hsm  24199  h2hnm  24200  hhsssm  24483  hhssnm  24484  eulerpartlemgvv  26606  eulerpartlemgh  26608  fprod2dlem  27337  br2ndeq  27432  heiborlem7  28557  heiborlem8  28558  pellexlem5  29016  pellex  29018  wlknwwlknsur  30187  wlkiswwlksur  30194  clwlkfoclwwlk  30361  dvhvaddass  34312  dvhlveclem  34323  diblss  34385
  Copyright terms: Public domain W3C validator