Theorem op2nd 7996

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {csn 4590  ⟨cop 4596  ∪ cuni 4873  ran crn 5664  ‘cfv 6538  2^nd c2nd 7986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fv 6546  df-2nd 7988

This theorem is referenced by:  op2ndd  7998  op2ndg  8000  2ndval2  8005  fo2ndres  8014  opreuopreu  8032  eloprabi  8061  fo2ndf  8117  f1o2ndf1  8118  seqomlem1  8438  seqomlem2  8439  xpmapenlem  9133  fseqenlem2  10010  axdc4lem  10440  iunfo  10524  archnq  10966  om2uzrdg  13994  uzrdgsuci  13998  fsum2dlem  15823  fprod2dlem  16036  ruclem8  16294  ruclem11  16297  eucalglt  16644  idfu2nd  17935  idfucl  17939  cofu2nd  17943  cofucl  17946  xpccatid  18245  prf2nd  18262  curf2ndf  18304  yonedalem22  18335  gaid  19370  2ndcctbss  23593  upxp  23761  uptx  23763  txkgen  23790  cnheiborlem  25094  ovollb2lem  25628  ovolctb  25630  ovoliunlem2  25643  ovolshftlem1  25649  ovolscalem1  25653  ovolicc1  25656  addsqnreup  27588  2sqreuop  27607  2sqreuopnn  27608  2sqreuoplt  27609  2sqreuopltb  27610  2sqreuopnnlt  27611  2sqreuopnnltb  27612  precsexlem2  28382  precsexlem5  28385  om2noseqrdg  28478  noseqrdgsuc  28482  wlkswwlksf1o  30209  clwlkclwwlkfo  30341  ex-2nd  30777  cnnvs  31013  cnnvnm  31014  h2hsm  31308  h2hnm  31309  hhsssm  31591  hhssnm  31592  2ndimaxp  32972  2ndresdju  32975  aciunf1lem  32988  gsumpart  33364  rlocf1  33575  fracfld  33610  eulerpartlemgvv  34747  eulerpartlemgh  34749  satfv0fvfmla0  35886  sategoelfvb  35892  prv1n  35904  msubff1  36029  msubvrs  36033  poimirlem17  38269  heiborlem7  38449  heiborlem8  38450  dvhvaddass  41852  dvhlveclem  41863  diblss  41925  aks6d1c3  42871  pellexlem5  43543  pellex  43545  dvnprodlem1  46643  hoicvr  47245  hoicvrrex  47253  ovn0lem  47262  ovnhoilem1  47298  ovnlecvr2  47307  ovolval5lem2  47350  gpg3kgrtriex  48837  pgnioedg1  48856  pgnioedg2  48857  pgnioedg3  48858  pgnioedg4  48859  pgnioedg5  48860  pgnbgreunbgrlem2lem1  48862  pgnbgreunbgrlem2lem2  48863  pgnbgreunbgrlem2lem3  48864  pgnbgreunbgrlem5lem1  48868  pgnbgreunbgrlem5lem2  48869  pgnbgreunbgrlem5lem3  48870  eloprab1st2nd  49629  swapf2fvala  50025  swapf2f1oaALT  50039  swapfcoa  50042  fuco21  50097  fucof21  50108  prcof2a  50150  prcof2  50151