Theorem op2nd 7068

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

Syntax hints:   = wceq 1475   ∈ wcel 1977  Vcvv 3173  {csn 4125  ⟨cop 4131  ∪ cuni 4372  ran crn 5039  ‘cfv 5804  2^nd c2nd 7058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fv 5812  df-2nd 7060

This theorem is referenced by:  op2ndd  7070  op2ndg  7072  2ndval2  7077  fo2ndres  7084  eloprabi  7121  fo2ndf  7171  f1o2ndf1  7172  seqomlem1  7432  seqomlem2  7433  xpmapenlem  8012  fseqenlem2  8731  axdc4lem  9160  iunfo  9240  archnq  9681  om2uzrdg  12617  uzrdgsuci  12621  fsum2dlem  14343  fprod2dlem  14549  ruclem8  14805  ruclem11  14808  eucalglt  15136  idfu2nd  16360  idfucl  16364  cofu2nd  16368  cofucl  16371  xpccatid  16651  prf2nd  16668  curf2ndf  16710  yonedalem22  16741  gaid  17555  2ndcctbss  21068  upxp  21236  uptx  21238  txkgen  21265  cnheiborlem  22561  ovollb2lem  23063  ovolctb  23065  ovoliunlem2  23078  ovolshftlem1  23084  ovolscalem1  23088  ovolicc1  23091  iedgvalsnop  25717  wlknwwlknsur  26240  wlkiswwlksur  26247  clwlkfoclwwlk  26372  ex-2nd  26694  cnnvs  26919  cnnvnm  26920  h2hsm  27216  h2hnm  27217  hhsssm  27499  hhssnm  27500  aciunf1lem  28844  eulerpartlemgvv  29765  eulerpartlemgh  29767  msubff1  30707  msubvrs  30711  br2ndeq  30918  poimirlem17  32596  heiborlem7  32786  heiborlem8  32787  dvhvaddass  35404  dvhlveclem  35415  diblss  35477  pellexlem5  36415  pellex  36417  dvnprodlem1  38836  hoicvr  39438  hoicvrrex  39446  ovn0lem  39455  ovnhoilem1  39491  ovnlecvr2  39500  ovolval5lem2  39543  1wlkpwwlkf1ouspgr  41076  wlknwwlksnsur  41087  wlkwwlksur  41094  clwlksfoclwwlk  41270