Theorem op2nd 7952

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3442  {csn 4582  ⟨cop 4588  ∪ cuni 4865  ran crn 5633  ‘cfv 6500  2^nd c2nd 7942

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 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fv 6508  df-2nd 7944

This theorem is referenced by:  op2ndd  7954  op2ndg  7956  2ndval2  7961  fo2ndres  7970  opreuopreu  7988  eloprabi  8017  fo2ndf  8073  f1o2ndf1  8074  seqomlem1  8391  seqomlem2  8392  xpmapenlem  9084  fseqenlem2  9947  axdc4lem  10377  iunfo  10461  archnq  10903  om2uzrdg  13891  uzrdgsuci  13895  fsum2dlem  15705  fprod2dlem  15915  ruclem8  16174  ruclem11  16177  eucalglt  16524  idfu2nd  17813  idfucl  17817  cofu2nd  17821  cofucl  17824  xpccatid  18123  prf2nd  18140  curf2ndf  18182  yonedalem22  18213  gaid  19240  2ndcctbss  23411  upxp  23579  uptx  23581  txkgen  23608  cnheiborlem  24921  ovollb2lem  25457  ovolctb  25459  ovoliunlem2  25472  ovolshftlem1  25478  ovolscalem1  25482  ovolicc1  25485  addsqnreup  27422  2sqreuop  27441  2sqreuopnn  27442  2sqreuoplt  27443  2sqreuopltb  27444  2sqreuopnnlt  27445  2sqreuopnnltb  27446  precsexlem2  28216  precsexlem5  28219  om2noseqrdg  28312  noseqrdgsuc  28316  wlkswwlksf1o  29964  clwlkclwwlkfo  30096  ex-2nd  30532  cnnvs  30767  cnnvnm  30768  h2hsm  31062  h2hnm  31063  hhsssm  31345  hhssnm  31346  2ndimaxp  32735  2ndresdju  32738  aciunf1lem  32751  gsumpart  33156  rlocf1  33366  fracfld  33401  eulerpartlemgvv  34553  eulerpartlemgh  34555  satfv0fvfmla0  35626  sategoelfvb  35632  prv1n  35644  msubff1  35769  msubvrs  35773  poimirlem17  37882  heiborlem7  38062  heiborlem8  38063  dvhvaddass  41467  dvhlveclem  41478  diblss  41540  aks6d1c3  42487  pellexlem5  43184  pellex  43186  dvnprodlem1  46298  hoicvr  46900  hoicvrrex  46908  ovn0lem  46917  ovnhoilem1  46953  ovnlecvr2  46962  ovolval5lem2  47005  gpg3kgrtriex  48443  pgnioedg1  48462  pgnioedg2  48463  pgnioedg3  48464  pgnioedg4  48465  pgnioedg5  48466  pgnbgreunbgrlem2lem1  48468  pgnbgreunbgrlem2lem2  48469  pgnbgreunbgrlem2lem3  48470  pgnbgreunbgrlem5lem1  48474  pgnbgreunbgrlem5lem2  48475  pgnbgreunbgrlem5lem3  48476  eloprab1st2nd  49221  swapf2fvala  49617  swapf2f1oaALT  49631  swapfcoa  49634  fuco21  49689  fucof21  49700  prcof2a  49742  prcof2  49743