Theorem op2nd 7701

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

Syntax hints:   = wceq 1536   ∈ wcel 2113  Vcvv 3497  {csn 4570  ⟨cop 4576  ∪ cuni 4841  ran crn 5559  ‘cfv 6358  2^nd c2nd 7691

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-iota 6317  df-fun 6360  df-fv 6366  df-2nd 7693

This theorem is referenced by:  op2ndd  7703  op2ndg  7705  2ndval2  7710  fo2ndres  7719  opreuopreu  7737  eloprabi  7764  fo2ndf  7820  f1o2ndf1  7821  seqomlem1  8089  seqomlem2  8090  xpmapenlem  8687  fseqenlem2  9454  axdc4lem  9880  iunfo  9964  archnq  10405  om2uzrdg  13327  uzrdgsuci  13331  fsum2dlem  15128  fprod2dlem  15337  ruclem8  15593  ruclem11  15596  eucalglt  15932  idfu2nd  17150  idfucl  17154  cofu2nd  17158  cofucl  17161  xpccatid  17441  prf2nd  17458  curf2ndf  17500  yonedalem22  17531  gaid  18432  2ndcctbss  22066  upxp  22234  uptx  22236  txkgen  22263  cnheiborlem  23561  ovollb2lem  24092  ovolctb  24094  ovoliunlem2  24107  ovolshftlem1  24113  ovolscalem1  24117  ovolicc1  24120  addsqnreup  26022  2sqreuop  26041  2sqreuopnn  26042  2sqreuoplt  26043  2sqreuopltb  26044  2sqreuopnnlt  26045  2sqreuopnnltb  26046  wlkswwlksf1o  27660  clwlkclwwlkfo  27790  ex-2nd  28227  cnnvs  28460  cnnvnm  28461  h2hsm  28755  h2hnm  28756  hhsssm  29038  hhssnm  29039  aciunf1lem  30410  eulerpartlemgvv  31638  eulerpartlemgh  31640  satfv0fvfmla0  32664  sategoelfvb  32670  prv1n  32682  msubff1  32807  msubvrs  32811  poimirlem17  34913  heiborlem7  35099  heiborlem8  35100  dvhvaddass  38237  dvhlveclem  38248  diblss  38310  pellexlem5  39436  pellex  39438  dvnprodlem1  42237  hoicvr  42837  hoicvrrex  42845  ovn0lem  42854  ovnhoilem1  42890  ovnlecvr2  42899  ovolval5lem2  42942