Theorem op2nd 7936

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3437  {csn 4575  ⟨cop 4581  ∪ cuni 4858  ran crn 5620  ‘cfv 6486  2^nd c2nd 7926

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6442  df-fun 6488  df-fv 6494  df-2nd 7928

This theorem is referenced by:  op2ndd  7938  op2ndg  7940  2ndval2  7945  fo2ndres  7954  opreuopreu  7972  eloprabi  8001  fo2ndf  8057  f1o2ndf1  8058  seqomlem1  8375  seqomlem2  8376  xpmapenlem  9064  fseqenlem2  9923  axdc4lem  10353  iunfo  10437  archnq  10878  om2uzrdg  13865  uzrdgsuci  13869  fsum2dlem  15679  fprod2dlem  15889  ruclem8  16148  ruclem11  16151  eucalglt  16498  idfu2nd  17786  idfucl  17790  cofu2nd  17794  cofucl  17797  xpccatid  18096  prf2nd  18113  curf2ndf  18155  yonedalem22  18186  gaid  19213  2ndcctbss  23371  upxp  23539  uptx  23541  txkgen  23568  cnheiborlem  24881  ovollb2lem  25417  ovolctb  25419  ovoliunlem2  25432  ovolshftlem1  25438  ovolscalem1  25442  ovolicc1  25445  addsqnreup  27382  2sqreuop  27401  2sqreuopnn  27402  2sqreuoplt  27403  2sqreuopltb  27404  2sqreuopnnlt  27405  2sqreuopnnltb  27406  precsexlem2  28147  precsexlem5  28150  om2noseqrdg  28235  noseqrdgsuc  28239  wlkswwlksf1o  29859  clwlkclwwlkfo  29991  ex-2nd  30427  cnnvs  30662  cnnvnm  30663  h2hsm  30957  h2hnm  30958  hhsssm  31240  hhssnm  31241  2ndimaxp  32630  2ndresdju  32633  aciunf1lem  32646  gsumpart  33044  rlocf1  33247  fracfld  33281  eulerpartlemgvv  34410  eulerpartlemgh  34412  satfv0fvfmla0  35478  sategoelfvb  35484  prv1n  35496  msubff1  35621  msubvrs  35625  poimirlem17  37697  heiborlem7  37877  heiborlem8  37878  dvhvaddass  41216  dvhlveclem  41227  diblss  41289  aks6d1c3  42236  pellexlem5  42950  pellex  42952  dvnprodlem1  46068  hoicvr  46670  hoicvrrex  46678  ovn0lem  46687  ovnhoilem1  46723  ovnlecvr2  46732  ovolval5lem2  46775  gpg3kgrtriex  48213  pgnioedg1  48232  pgnioedg2  48233  pgnioedg3  48234  pgnioedg4  48235  pgnioedg5  48236  pgnbgreunbgrlem2lem1  48238  pgnbgreunbgrlem2lem2  48239  pgnbgreunbgrlem2lem3  48240  pgnbgreunbgrlem5lem1  48244  pgnbgreunbgrlem5lem2  48245  pgnbgreunbgrlem5lem3  48246  eloprab1st2nd  48992  swapf2fvala  49389  swapf2f1oaALT  49403  swapfcoa  49406  fuco21  49461  fucof21  49472  prcof2a  49514  prcof2  49515