Theorem op2nd 7343

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

Syntax hints:   = wceq 1632   ∈ wcel 2139  Vcvv 3340  {csn 4321  ⟨cop 4327  ∪ cuni 4588  ran crn 5267  ‘cfv 6049  2^nd c2nd 7333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-iota 6012  df-fun 6051  df-fv 6057  df-2nd 7335

This theorem is referenced by:  op2ndd  7345  op2ndg  7347  2ndval2  7352  fo2ndres  7361  eloprabi  7401  fo2ndf  7453  f1o2ndf1  7454  seqomlem1  7715  seqomlem2  7716  xpmapenlem  8294  fseqenlem2  9058  axdc4lem  9489  iunfo  9573  archnq  10014  om2uzrdg  12969  uzrdgsuci  12973  fsum2dlem  14720  fprod2dlem  14929  ruclem8  15185  ruclem11  15188  eucalglt  15520  idfu2nd  16758  idfucl  16762  cofu2nd  16766  cofucl  16769  xpccatid  17049  prf2nd  17066  curf2ndf  17108  yonedalem22  17139  gaid  17952  2ndcctbss  21480  upxp  21648  uptx  21650  txkgen  21677  cnheiborlem  22974  ovollb2lem  23476  ovolctb  23478  ovoliunlem2  23491  ovolshftlem1  23497  ovolscalem1  23501  ovolicc1  23504  wlkpwwlkf1ouspgr  27009  wlknwwlksnsur  27020  wlkwwlksur  27027  clwlkclwwlkfo  27153  clwlksfoclwwlkOLD  27238  ex-2nd  27634  cnnvs  27865  cnnvnm  27866  h2hsm  28162  h2hnm  28163  hhsssm  28445  hhssnm  28446  aciunf1lem  29792  eulerpartlemgvv  30768  eulerpartlemgh  30770  msubff1  31781  msubvrs  31785  poimirlem17  33757  heiborlem7  33947  heiborlem8  33948  dvhvaddass  36906  dvhlveclem  36917  diblss  36979  pellexlem5  37917  pellex  37919  dvnprodlem1  40682  hoicvr  41286  hoicvrrex  41294  ovn0lem  41303  ovnhoilem1  41339  ovnlecvr2  41348  ovolval5lem2  41391