Theorem op2nd 7748

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

Syntax hints:   = wceq 1543   ∈ wcel 2112  Vcvv 3398  {csn 4527  ⟨cop 4533  ∪ cuni 4805  ran crn 5537  ‘cfv 6358  2^nd c2nd 7738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-iota 6316  df-fun 6360  df-fv 6366  df-2nd 7740

This theorem is referenced by:  op2ndd  7750  op2ndg  7752  2ndval2  7757  fo2ndres  7766  opreuopreu  7784  eloprabi  7811  fo2ndf  7868  f1o2ndf1  7869  seqomlem1  8164  seqomlem2  8165  xpmapenlem  8791  fseqenlem2  9604  axdc4lem  10034  iunfo  10118  archnq  10559  om2uzrdg  13494  uzrdgsuci  13498  fsum2dlem  15297  fprod2dlem  15505  ruclem8  15761  ruclem11  15764  eucalglt  16105  idfu2nd  17337  idfucl  17341  cofu2nd  17345  cofucl  17348  xpccatid  17649  prf2nd  17666  curf2ndf  17709  yonedalem22  17740  gaid  18647  2ndcctbss  22306  upxp  22474  uptx  22476  txkgen  22503  cnheiborlem  23805  ovollb2lem  24339  ovolctb  24341  ovoliunlem2  24354  ovolshftlem1  24360  ovolscalem1  24364  ovolicc1  24367  addsqnreup  26278  2sqreuop  26297  2sqreuopnn  26298  2sqreuoplt  26299  2sqreuopltb  26300  2sqreuopnnlt  26301  2sqreuopnnltb  26302  wlkswwlksf1o  27917  clwlkclwwlkfo  28046  ex-2nd  28482  cnnvs  28715  cnnvnm  28716  h2hsm  29010  h2hnm  29011  hhsssm  29293  hhssnm  29294  2ndimaxp  30657  2ndresdju  30659  aciunf1lem  30673  gsumpart  30988  eulerpartlemgvv  32009  eulerpartlemgh  32011  satfv0fvfmla0  33042  sategoelfvb  33048  prv1n  33060  msubff1  33185  msubvrs  33189  ot22ndd  33351  poimirlem17  35480  heiborlem7  35661  heiborlem8  35662  dvhvaddass  38797  dvhlveclem  38808  diblss  38870  pellexlem5  40299  pellex  40301  dvnprodlem1  43105  hoicvr  43704  hoicvrrex  43712  ovn0lem  43721  ovnhoilem1  43757  ovnlecvr2  43766  ovolval5lem2  43809