Theorem op2nd 7977

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3447  {csn 4589  ⟨cop 4595  ∪ cuni 4871  ran crn 5639  ‘cfv 6511  2^nd c2nd 7967

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fv 6519  df-2nd 7969

This theorem is referenced by:  op2ndd  7979  op2ndg  7981  2ndval2  7986  fo2ndres  7995  opreuopreu  8013  eloprabi  8042  fo2ndf  8100  f1o2ndf1  8101  seqomlem1  8418  seqomlem2  8419  xpmapenlem  9108  fseqenlem2  9978  axdc4lem  10408  iunfo  10492  archnq  10933  om2uzrdg  13921  uzrdgsuci  13925  fsum2dlem  15736  fprod2dlem  15946  ruclem8  16205  ruclem11  16208  eucalglt  16555  idfu2nd  17839  idfucl  17843  cofu2nd  17847  cofucl  17850  xpccatid  18149  prf2nd  18166  curf2ndf  18208  yonedalem22  18239  gaid  19231  2ndcctbss  23342  upxp  23510  uptx  23512  txkgen  23539  cnheiborlem  24853  ovollb2lem  25389  ovolctb  25391  ovoliunlem2  25404  ovolshftlem1  25410  ovolscalem1  25414  ovolicc1  25417  addsqnreup  27354  2sqreuop  27373  2sqreuopnn  27374  2sqreuoplt  27375  2sqreuopltb  27376  2sqreuopnnlt  27377  2sqreuopnnltb  27378  precsexlem2  28110  precsexlem5  28113  om2noseqrdg  28198  noseqrdgsuc  28202  wlkswwlksf1o  29809  clwlkclwwlkfo  29938  ex-2nd  30374  cnnvs  30609  cnnvnm  30610  h2hsm  30904  h2hnm  30905  hhsssm  31187  hhssnm  31188  2ndimaxp  32570  2ndresdju  32573  aciunf1lem  32586  gsumpart  32997  rlocf1  33224  fracfld  33258  eulerpartlemgvv  34367  eulerpartlemgh  34369  satfv0fvfmla0  35400  sategoelfvb  35406  prv1n  35418  msubff1  35543  msubvrs  35547  poimirlem17  37631  heiborlem7  37811  heiborlem8  37812  dvhvaddass  41091  dvhlveclem  41102  diblss  41164  aks6d1c3  42111  pellexlem5  42821  pellex  42823  dvnprodlem1  45944  hoicvr  46546  hoicvrrex  46554  ovn0lem  46563  ovnhoilem1  46599  ovnlecvr2  46608  ovolval5lem2  46651  gpg3kgrtriex  48080  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  eloprab1st2nd  48856  swapf2fvala  49253  swapf2f1oaALT  49267  swapfcoa  49270  fuco21  49325  fucof21  49336  prcof2a  49378  prcof2  49379