Theorem op2nd 7930

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {csn 4576  ⟨cop 4582  ∪ cuni 4859  ran crn 5617  ‘cfv 6481  2^nd c2nd 7920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-iota 6437  df-fun 6483  df-fv 6489  df-2nd 7922

This theorem is referenced by:  op2ndd  7932  op2ndg  7934  2ndval2  7939  fo2ndres  7948  opreuopreu  7966  eloprabi  7995  fo2ndf  8051  f1o2ndf1  8052  seqomlem1  8369  seqomlem2  8370  xpmapenlem  9057  fseqenlem2  9913  axdc4lem  10343  iunfo  10427  archnq  10868  om2uzrdg  13860  uzrdgsuci  13864  fsum2dlem  15674  fprod2dlem  15884  ruclem8  16143  ruclem11  16146  eucalglt  16493  idfu2nd  17781  idfucl  17785  cofu2nd  17789  cofucl  17792  xpccatid  18091  prf2nd  18108  curf2ndf  18150  yonedalem22  18181  gaid  19209  2ndcctbss  23368  upxp  23536  uptx  23538  txkgen  23565  cnheiborlem  24878  ovollb2lem  25414  ovolctb  25416  ovoliunlem2  25429  ovolshftlem1  25435  ovolscalem1  25439  ovolicc1  25442  addsqnreup  27379  2sqreuop  27398  2sqreuopnn  27399  2sqreuoplt  27400  2sqreuopltb  27401  2sqreuopnnlt  27402  2sqreuopnnltb  27403  precsexlem2  28144  precsexlem5  28147  om2noseqrdg  28232  noseqrdgsuc  28236  wlkswwlksf1o  29855  clwlkclwwlkfo  29984  ex-2nd  30420  cnnvs  30655  cnnvnm  30656  h2hsm  30950  h2hnm  30951  hhsssm  31233  hhssnm  31234  2ndimaxp  32623  2ndresdju  32626  aciunf1lem  32639  gsumpart  33032  rlocf1  33235  fracfld  33269  eulerpartlemgvv  34384  eulerpartlemgh  34386  satfv0fvfmla0  35445  sategoelfvb  35451  prv1n  35463  msubff1  35588  msubvrs  35592  poimirlem17  37676  heiborlem7  37856  heiborlem8  37857  dvhvaddass  41135  dvhlveclem  41146  diblss  41208  aks6d1c3  42155  pellexlem5  42865  pellex  42867  dvnprodlem1  45983  hoicvr  46585  hoicvrrex  46593  ovn0lem  46602  ovnhoilem1  46638  ovnlecvr2  46647  ovolval5lem2  46690  gpg3kgrtriex  48119  pgnioedg1  48138  pgnioedg2  48139  pgnioedg3  48140  pgnioedg4  48141  pgnioedg5  48142  pgnbgreunbgrlem2lem1  48144  pgnbgreunbgrlem2lem2  48145  pgnbgreunbgrlem2lem3  48146  pgnbgreunbgrlem5lem1  48150  pgnbgreunbgrlem5lem2  48151  pgnbgreunbgrlem5lem3  48152  eloprab1st2nd  48898  swapf2fvala  49295  swapf2f1oaALT  49309  swapfcoa  49312  fuco21  49367  fucof21  49378  prcof2a  49420  prcof2  49421