Theorem op2nd 8023

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3480  {csn 4626  ⟨cop 4632  ∪ cuni 4907  ran crn 5686  ‘cfv 6561  2^nd c2nd 8013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-2nd 8015

This theorem is referenced by:  op2ndd  8025  op2ndg  8027  2ndval2  8032  fo2ndres  8041  opreuopreu  8059  eloprabi  8088  fo2ndf  8146  f1o2ndf1  8147  seqomlem1  8490  seqomlem2  8491  xpmapenlem  9184  fseqenlem2  10065  axdc4lem  10495  iunfo  10579  archnq  11020  om2uzrdg  13997  uzrdgsuci  14001  fsum2dlem  15806  fprod2dlem  16016  ruclem8  16273  ruclem11  16276  eucalglt  16622  idfu2nd  17922  idfucl  17926  cofu2nd  17930  cofucl  17933  xpccatid  18233  prf2nd  18250  curf2ndf  18292  yonedalem22  18323  gaid  19317  2ndcctbss  23463  upxp  23631  uptx  23633  txkgen  23660  cnheiborlem  24986  ovollb2lem  25523  ovolctb  25525  ovoliunlem2  25538  ovolshftlem1  25544  ovolscalem1  25548  ovolicc1  25551  addsqnreup  27487  2sqreuop  27506  2sqreuopnn  27507  2sqreuoplt  27508  2sqreuopltb  27509  2sqreuopnnlt  27510  2sqreuopnnltb  27511  precsexlem2  28232  precsexlem5  28235  om2noseqrdg  28310  noseqrdgsuc  28314  wlkswwlksf1o  29899  clwlkclwwlkfo  30028  ex-2nd  30464  cnnvs  30699  cnnvnm  30700  h2hsm  30994  h2hnm  30995  hhsssm  31277  hhssnm  31278  2ndimaxp  32656  2ndresdju  32659  aciunf1lem  32672  gsumpart  33060  rlocf1  33277  fracfld  33310  eulerpartlemgvv  34378  eulerpartlemgh  34380  satfv0fvfmla0  35418  sategoelfvb  35424  prv1n  35436  msubff1  35561  msubvrs  35565  poimirlem17  37644  heiborlem7  37824  heiborlem8  37825  dvhvaddass  41099  dvhlveclem  41110  diblss  41172  aks6d1c3  42124  pellexlem5  42844  pellex  42846  dvnprodlem1  45961  hoicvr  46563  hoicvrrex  46571  ovn0lem  46580  ovnhoilem1  46616  ovnlecvr2  46625  ovolval5lem2  46668  gpg3kgrtriex  48045  swapf2fvala  48970  swapf2f1oaALT  48984  swapfcoa  48987  fuco21  49031  fucof21  49042