Theorem op2nd 7951

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3429  {csn 4567  ⟨cop 4573  ∪ cuni 4850  ran crn 5632  ‘cfv 6498  2^nd c2nd 7941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fv 6506  df-2nd 7943

This theorem is referenced by:  op2ndd  7953  op2ndg  7955  2ndval2  7960  fo2ndres  7969  opreuopreu  7987  eloprabi  8016  fo2ndf  8071  f1o2ndf1  8072  seqomlem1  8389  seqomlem2  8390  xpmapenlem  9082  fseqenlem2  9947  axdc4lem  10377  iunfo  10461  archnq  10903  om2uzrdg  13918  uzrdgsuci  13922  fsum2dlem  15732  fprod2dlem  15945  ruclem8  16204  ruclem11  16207  eucalglt  16554  idfu2nd  17844  idfucl  17848  cofu2nd  17852  cofucl  17855  xpccatid  18154  prf2nd  18171  curf2ndf  18213  yonedalem22  18244  gaid  19274  2ndcctbss  23420  upxp  23588  uptx  23590  txkgen  23617  cnheiborlem  24921  ovollb2lem  25455  ovolctb  25457  ovoliunlem2  25470  ovolshftlem1  25476  ovolscalem1  25480  ovolicc1  25483  addsqnreup  27406  2sqreuop  27425  2sqreuopnn  27426  2sqreuoplt  27427  2sqreuopltb  27428  2sqreuopnnlt  27429  2sqreuopnnltb  27430  precsexlem2  28200  precsexlem5  28203  om2noseqrdg  28296  noseqrdgsuc  28300  wlkswwlksf1o  29947  clwlkclwwlkfo  30079  ex-2nd  30515  cnnvs  30751  cnnvnm  30752  h2hsm  31046  h2hnm  31047  hhsssm  31329  hhssnm  31330  2ndimaxp  32719  2ndresdju  32722  aciunf1lem  32735  gsumpart  33124  rlocf1  33334  fracfld  33369  eulerpartlemgvv  34520  eulerpartlemgh  34522  satfv0fvfmla0  35595  sategoelfvb  35601  prv1n  35613  msubff1  35738  msubvrs  35742  poimirlem17  37958  heiborlem7  38138  heiborlem8  38139  dvhvaddass  41543  dvhlveclem  41554  diblss  41616  aks6d1c3  42562  pellexlem5  43261  pellex  43263  dvnprodlem1  46374  hoicvr  46976  hoicvrrex  46984  ovn0lem  46993  ovnhoilem1  47029  ovnlecvr2  47038  ovolval5lem2  47081  gpg3kgrtriex  48565  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  eloprab1st2nd  49343  swapf2fvala  49739  swapf2f1oaALT  49753  swapfcoa  49756  fuco21  49811  fucof21  49822  prcof2a  49864  prcof2  49865