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

Theorem op2nd 6695
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 6689 . 2  |-  ( 2nd `  <. A ,  B >. )  =  U. ran  {
<. A ,  B >. }
2 op1st.1 . . 3  |-  A  e. 
_V
3 op1st.2 . . 3  |-  B  e. 
_V
42, 3op2nda 5431 . 2  |-  U. ran  {
<. A ,  B >. }  =  B
51, 4eqtri 2483 1  |-  ( 2nd `  <. A ,  B >. )  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    e. wcel 1758   _Vcvv 3076   {csn 3984   <.cop 3990   U.cuni 4198   ran crn 4948   ` cfv 5525   2ndc2nd 6685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-iota 5488  df-fun 5527  df-fv 5533  df-2nd 6687
This theorem is referenced by:  op2ndd  6697  op2ndg  6699  2ndval2  6704  fo2ndres  6710  eloprabi  6745  fo2ndf  6788  f1o2ndf1  6789  seqomlem1  7014  seqomlem2  7015  xpmapenlem  7587  fseqenlem2  8305  axdc4lem  8734  iunfo  8813  archnq  9259  om2uzrdg  11895  uzrdgsuci  11899  fsum2dlem  13354  ruclem8  13636  ruclem11  13639  eucalglt  13877  idfu2nd  14905  idfucl  14909  cofu2nd  14913  cofucl  14916  xpccatid  15116  prf2nd  15133  curf2ndf  15175  yonedalem22  15206  gaid  15935  2ndcctbss  19190  upxp  19327  uptx  19329  txkgen  19356  cnheiborlem  20657  ovollb2lem  21102  ovolctb  21104  ovoliunlem2  21117  ovolshftlem1  21123  ovolscalem1  21127  ovolicc1  21130  ex-2nd  23803  cnnvs  24222  cnnvnm  24223  h2hsm  24528  h2hnm  24529  hhsssm  24812  hhssnm  24813  eulerpartlemgvv  26902  eulerpartlemgh  26904  fprod2dlem  27634  br2ndeq  27729  heiborlem7  28863  heiborlem8  28864  pellexlem5  29321  pellex  29323  wlknwwlknsur  30491  wlkiswwlksur  30498  clwlkfoclwwlk  30665  dvhvaddass  35065  dvhlveclem  35076  diblss  35138
  Copyright terms: Public domain W3C validator