Theorem op2nd 8022

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

Syntax hints:   = wceq 1537   ∈ wcel 2106  Vcvv 3478  {csn 4631  ⟨cop 4637  ∪ cuni 4912  ran crn 5690  ‘cfv 6563  2^nd c2nd 8012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fv 6571  df-2nd 8014

This theorem is referenced by:  op2ndd  8024  op2ndg  8026  2ndval2  8031  fo2ndres  8040  opreuopreu  8058  eloprabi  8087  fo2ndf  8145  f1o2ndf1  8146  seqomlem1  8489  seqomlem2  8490  xpmapenlem  9183  fseqenlem2  10063  axdc4lem  10493  iunfo  10577  archnq  11018  om2uzrdg  13994  uzrdgsuci  13998  fsum2dlem  15803  fprod2dlem  16013  ruclem8  16270  ruclem11  16273  eucalglt  16619  idfu2nd  17928  idfucl  17932  cofu2nd  17936  cofucl  17939  xpccatid  18244  prf2nd  18261  curf2ndf  18304  yonedalem22  18335  gaid  19330  2ndcctbss  23479  upxp  23647  uptx  23649  txkgen  23676  cnheiborlem  25000  ovollb2lem  25537  ovolctb  25539  ovoliunlem2  25552  ovolshftlem1  25558  ovolscalem1  25562  ovolicc1  25565  addsqnreup  27502  2sqreuop  27521  2sqreuopnn  27522  2sqreuoplt  27523  2sqreuopltb  27524  2sqreuopnnlt  27525  2sqreuopnnltb  27526  precsexlem2  28247  precsexlem5  28250  om2noseqrdg  28325  noseqrdgsuc  28329  wlkswwlksf1o  29909  clwlkclwwlkfo  30038  ex-2nd  30474  cnnvs  30709  cnnvnm  30710  h2hsm  31004  h2hnm  31005  hhsssm  31287  hhssnm  31288  2ndimaxp  32663  2ndresdju  32666  aciunf1lem  32679  gsumpart  33043  rlocf1  33260  fracfld  33290  eulerpartlemgvv  34358  eulerpartlemgh  34360  satfv0fvfmla0  35398  sategoelfvb  35404  prv1n  35416  msubff1  35541  msubvrs  35545  poimirlem17  37624  heiborlem7  37804  heiborlem8  37805  dvhvaddass  41080  dvhlveclem  41091  diblss  41153  aks6d1c3  42105  pellexlem5  42821  pellex  42823  dvnprodlem1  45902  hoicvr  46504  hoicvrrex  46512  ovn0lem  46521  ovnhoilem1  46557  ovnlecvr2  46566  ovolval5lem2  46609