Theorem op2nd 7975

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 7969	. 2 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = ∪ ran {⟨𝐴, 𝐵⟩}
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op2nda 6211	. 2 ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
5	1, 4	eqtri 2784	1 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵

Syntax hints:   = wceq 1559   ∈ wcel 2141  Vcvv 3453  {csn 4581  ⟨cop 4587  ∪ cuni 4864  ran crn 5646  ‘cfv 6517  2^nd c2nd 7965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fv 6525  df-2nd 7967

This theorem is referenced by:  op2ndd  7977  op2ndg  7979  2ndval2  7984  fo2ndres  7993  opreuopreu  8011  eloprabi  8040  fo2ndf  8095  f1o2ndf1  8096  seqomlem1  8416  seqomlem2  8417  xpmapenlem  9112  fseqenlem2  9978  axdc4lem  10409  iunfo  10493  archnq  10935  om2uzrdg  13966  uzrdgsuci  13970  fsum2dlem  15780  fprod2dlem  15993  ruclem8  16252  ruclem11  16255  eucalglt  16602  idfu2nd  17893  idfucl  17897  cofu2nd  17901  cofucl  17904  xpccatid  18203  prf2nd  18220  curf2ndf  18262  yonedalem22  18293  gaid  19322  2ndcctbss  23495  upxp  23663  uptx  23665  txkgen  23692  cnheiborlem  24996  ovollb2lem  25530  ovolctb  25532  ovoliunlem2  25545  ovolshftlem1  25551  ovolscalem1  25555  ovolicc1  25558  addsqnreup  27484  2sqreuop  27503  2sqreuopnn  27504  2sqreuoplt  27505  2sqreuopltb  27506  2sqreuopnnlt  27507  2sqreuopnnltb  27508  precsexlem2  28278  precsexlem5  28281  om2noseqrdg  28374  noseqrdgsuc  28378  wlkswwlksf1o  30025  clwlkclwwlkfo  30157  ex-2nd  30593  cnnvs  30829  cnnvnm  30830  h2hsm  31124  h2hnm  31125  hhsssm  31407  hhssnm  31408  2ndimaxp  32798  2ndresdju  32801  aciunf1lem  32814  gsumpart  33204  rlocf1  33416  fracfld  33456  eulerpartlemgvv  34634  eulerpartlemgh  34636  satfv0fvfmla0  35727  sategoelfvb  35733  prv1n  35745  msubff1  35870  msubvrs  35874  poimirlem17  38100  heiborlem7  38280  heiborlem8  38281  dvhvaddass  41685  dvhlveclem  41696  diblss  41758  aks6d1c3  42704  pellexlem5  43374  pellex  43376  dvnprodlem1  46484  hoicvr  47086  hoicvrrex  47094  ovn0lem  47103  ovnhoilem1  47139  ovnlecvr2  47148  ovolval5lem2  47191  gpg3kgrtriex  48675  pgnioedg1  48694  pgnioedg2  48695  pgnioedg3  48696  pgnioedg4  48697  pgnioedg5  48698  pgnbgreunbgrlem2lem1  48700  pgnbgreunbgrlem2lem2  48701  pgnbgreunbgrlem2lem3  48702  pgnbgreunbgrlem5lem1  48706  pgnbgreunbgrlem5lem2  48707  pgnbgreunbgrlem5lem3  48708  eloprab1st2nd  49453  swapf2fvala  49849  swapf2f1oaALT  49863  swapfcoa  49866  fuco21  49921  fucof21  49932  prcof2a  49974  prcof2  49975