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

Theorem op2nd 7375
Description: Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
Hypotheses
Ref Expression
op1st.1 𝐴 ∈ V
op1st.2 𝐵 ∈ V
Assertion
Ref Expression
op2nd (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵

Proof of Theorem op2nd
StepHypRef Expression
1 2ndval 7369 . 2 (2nd ‘⟨𝐴, 𝐵⟩) = ran {⟨𝐴, 𝐵⟩}
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op2nda 5806 . 2 ran {⟨𝐴, 𝐵⟩} = 𝐵
51, 4eqtri 2787 1 (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  wcel 2155  Vcvv 3350  {csn 4334  cop 4340   cuni 4594  ran crn 5278  cfv 6068  2nd c2nd 7365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-iota 6031  df-fun 6070  df-fv 6076  df-2nd 7367
This theorem is referenced by:  op2ndd  7377  op2ndg  7379  2ndval2  7384  fo2ndres  7393  eloprabi  7433  fo2ndf  7486  f1o2ndf1  7487  seqomlem1  7749  seqomlem2  7750  xpmapenlem  8334  fseqenlem2  9099  axdc4lem  9530  iunfo  9614  archnq  10055  om2uzrdg  12963  uzrdgsuci  12967  fsum2dlem  14788  fprod2dlem  14995  ruclem8  15250  ruclem11  15253  eucalglt  15581  idfu2nd  16804  idfucl  16808  cofu2nd  16812  cofucl  16815  xpccatid  17096  prf2nd  17113  curf2ndf  17155  yonedalem22  17186  gaid  17997  2ndcctbss  21538  upxp  21706  uptx  21708  txkgen  21735  cnheiborlem  23032  ovollb2lem  23546  ovolctb  23548  ovoliunlem2  23561  ovolshftlem1  23567  ovolscalem1  23571  ovolicc1  23574  wlkswwlksf1o  27069  wlknwwlksnsurOLD  27080  wlkwwlksurOLD  27088  clwlkclwwlkfo  27215  clwlksfoclwwlkOLD  27300  ex-2nd  27696  cnnvs  27926  cnnvnm  27927  h2hsm  28223  h2hnm  28224  hhsssm  28506  hhssnm  28507  aciunf1lem  29847  eulerpartlemgvv  30820  eulerpartlemgh  30822  msubff1  31833  msubvrs  31837  poimirlem17  33782  heiborlem7  33970  heiborlem8  33971  dvhvaddass  36985  dvhlveclem  36996  diblss  37058  pellexlem5  38007  pellex  38009  dvnprodlem1  40731  hoicvr  41334  hoicvrrex  41342  ovn0lem  41351  ovnhoilem1  41387  ovnlecvr2  41396  ovolval5lem2  41439
  Copyright terms: Public domain W3C validator