Theorem op2nd 7981

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

Syntax hints:   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4628  ⟨cop 4634  ∪ cuni 4908  ran crn 5677  ‘cfv 6541  2^nd c2nd 7971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6493  df-fun 6543  df-fv 6549  df-2nd 7973

This theorem is referenced by:  op2ndd  7983  op2ndg  7985  2ndval2  7990  fo2ndres  7999  opreuopreu  8017  eloprabi  8046  fo2ndf  8104  f1o2ndf1  8105  seqomlem1  8447  seqomlem2  8448  xpmapenlem  9141  fseqenlem2  10017  axdc4lem  10447  iunfo  10531  archnq  10972  om2uzrdg  13918  uzrdgsuci  13922  fsum2dlem  15713  fprod2dlem  15921  ruclem8  16177  ruclem11  16180  eucalglt  16519  idfu2nd  17824  idfucl  17828  cofu2nd  17832  cofucl  17835  xpccatid  18137  prf2nd  18154  curf2ndf  18197  yonedalem22  18228  gaid  19158  2ndcctbss  22951  upxp  23119  uptx  23121  txkgen  23148  cnheiborlem  24462  ovollb2lem  24997  ovolctb  24999  ovoliunlem2  25012  ovolshftlem1  25018  ovolscalem1  25022  ovolicc1  25025  addsqnreup  26936  2sqreuop  26955  2sqreuopnn  26956  2sqreuoplt  26957  2sqreuopltb  26958  2sqreuopnnlt  26959  2sqreuopnnltb  26960  precsexlem2  27644  precsexlem5  27647  wlkswwlksf1o  29123  clwlkclwwlkfo  29252  ex-2nd  29688  cnnvs  29921  cnnvnm  29922  h2hsm  30216  h2hnm  30217  hhsssm  30499  hhssnm  30500  2ndimaxp  31860  2ndresdju  31862  aciunf1lem  31875  gsumpart  32195  eulerpartlemgvv  33364  eulerpartlemgh  33366  satfv0fvfmla0  34393  sategoelfvb  34399  prv1n  34411  msubff1  34536  msubvrs  34540  poimirlem17  36494  heiborlem7  36674  heiborlem8  36675  dvhvaddass  39957  dvhlveclem  39968  diblss  40030  pellexlem5  41557  pellex  41559  dvnprodlem1  44649  hoicvr  45251  hoicvrrex  45259  ovn0lem  45268  ovnhoilem1  45304  ovnlecvr2  45313  ovolval5lem2  45356