Theorem op2nd 7995

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  Vcvv 3463  {csn 4594  ⟨cop 4600  ∪ cuni 4876  ran crn 5663  ‘cfv 6537  2^nd c2nd 7985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-iota 6493  df-fun 6539  df-fv 6545  df-2nd 7987

This theorem is referenced by:  op2ndd  7997  op2ndg  7999  2ndval2  8004  fo2ndres  8013  opreuopreu  8031  eloprabi  8060  fo2ndf  8116  f1o2ndf1  8117  seqomlem1  8437  seqomlem2  8438  xpmapenlem  9132  fseqenlem2  10009  axdc4lem  10439  iunfo  10523  archnq  10965  om2uzrdg  13992  uzrdgsuci  13996  fsum2dlem  15821  fprod2dlem  16034  ruclem8  16293  ruclem11  16296  eucalglt  16643  idfu2nd  17934  idfucl  17938  cofu2nd  17942  cofucl  17945  xpccatid  18244  prf2nd  18261  curf2ndf  18303  yonedalem22  18334  gaid  19369  2ndcctbss  23581  upxp  23749  uptx  23751  txkgen  23778  cnheiborlem  25082  ovollb2lem  25616  ovolctb  25618  ovoliunlem2  25631  ovolshftlem1  25637  ovolscalem1  25641  ovolicc1  25644  addsqnreup  27573  2sqreuop  27592  2sqreuopnn  27593  2sqreuoplt  27594  2sqreuopltb  27595  2sqreuopnnlt  27596  2sqreuopnnltb  27597  precsexlem2  28367  precsexlem5  28370  om2noseqrdg  28463  noseqrdgsuc  28467  wlkswwlksf1o  30169  clwlkclwwlkfo  30301  ex-2nd  30737  cnnvs  30973  cnnvnm  30974  h2hsm  31268  h2hnm  31269  hhsssm  31551  hhssnm  31552  2ndimaxp  32932  2ndresdju  32935  aciunf1lem  32948  gsumpart  33324  rlocf1  33535  fracfld  33572  eulerpartlemgvv  34711  eulerpartlemgh  34713  satfv0fvfmla0  35838  sategoelfvb  35844  prv1n  35856  msubff1  35981  msubvrs  35985  poimirlem17  38210  heiborlem7  38390  heiborlem8  38391  dvhvaddass  41795  dvhlveclem  41806  diblss  41868  aks6d1c3  42814  pellexlem5  43486  pellex  43488  dvnprodlem1  46586  hoicvr  47188  hoicvrrex  47196  ovn0lem  47205  ovnhoilem1  47241  ovnlecvr2  47250  ovolval5lem2  47293  gpg3kgrtriex  48777  pgnioedg1  48796  pgnioedg2  48797  pgnioedg3  48798  pgnioedg4  48799  pgnioedg5  48800  pgnbgreunbgrlem2lem1  48802  pgnbgreunbgrlem2lem2  48803  pgnbgreunbgrlem2lem3  48804  pgnbgreunbgrlem5lem1  48808  pgnbgreunbgrlem5lem2  48809  pgnbgreunbgrlem5lem3  48810  eloprab1st2nd  49565  swapf2fvala  49961  swapf2f1oaALT  49975  swapfcoa  49978  fuco21  50033  fucof21  50044  prcof2a  50086  prcof2  50087