Theorem op2nd 8001

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

Step	Hyp	Ref	Expression
1		2ndval 7995	. 2 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = ∪ ran {⟨𝐴, 𝐵⟩}
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op2nda 6232	. 2 ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
5	1, 4	eqtri 2753	1 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵

Syntax hints:   = wceq 1533   ∈ wcel 2098  Vcvv 3463  {csn 4629  ⟨cop 4635  ∪ cuni 4908  ran crn 5678  ‘cfv 6547  2^nd c2nd 7991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pr 5428  ax-un 7739

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6499  df-fun 6549  df-fv 6555  df-2nd 7993

This theorem is referenced by:  op2ndd  8003  op2ndg  8005  2ndval2  8010  fo2ndres  8019  opreuopreu  8037  eloprabi  8066  fo2ndf  8124  f1o2ndf1  8125  seqomlem1  8469  seqomlem2  8470  xpmapenlem  9167  fseqenlem2  10048  axdc4lem  10478  iunfo  10562  archnq  11003  om2uzrdg  13953  uzrdgsuci  13957  fsum2dlem  15748  fprod2dlem  15956  ruclem8  16213  ruclem11  16216  eucalglt  16555  idfu2nd  17862  idfucl  17866  cofu2nd  17870  cofucl  17873  xpccatid  18178  prf2nd  18195  curf2ndf  18238  yonedalem22  18269  gaid  19254  2ndcctbss  23389  upxp  23557  uptx  23559  txkgen  23586  cnheiborlem  24910  ovollb2lem  25447  ovolctb  25449  ovoliunlem2  25462  ovolshftlem1  25468  ovolscalem1  25472  ovolicc1  25475  addsqnreup  27406  2sqreuop  27425  2sqreuopnn  27426  2sqreuoplt  27427  2sqreuopltb  27428  2sqreuopnnlt  27429  2sqreuopnnltb  27430  precsexlem2  28140  precsexlem5  28143  om2noseqrdg  28211  noseqrdgsuc  28215  wlkswwlksf1o  29746  clwlkclwwlkfo  29875  ex-2nd  30311  cnnvs  30546  cnnvnm  30547  h2hsm  30841  h2hnm  30842  hhsssm  31124  hhssnm  31125  2ndimaxp  32490  2ndresdju  32492  aciunf1lem  32505  gsumpart  32826  rlocf1  33027  fracfld  33055  eulerpartlemgvv  34066  eulerpartlemgh  34068  satfv0fvfmla0  35093  sategoelfvb  35099  prv1n  35111  msubff1  35236  msubvrs  35240  poimirlem17  37180  heiborlem7  37360  heiborlem8  37361  dvhvaddass  40639  dvhlveclem  40650  diblss  40712  aks6d1c3  41663  pellexlem5  42318  pellex  42320  dvnprodlem1  45397  hoicvr  45999  hoicvrrex  46007  ovn0lem  46016  ovnhoilem1  46052  ovnlecvr2  46061  ovolval5lem2  46104