Theorem op2nd 7509

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

Syntax hints:   = wceq 1508   ∈ wcel 2051  Vcvv 3410  {csn 4436  ⟨cop 4442  ∪ cuni 4709  ran crn 5405  ‘cfv 6186  2^nd c2nd 7499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-iota 6150  df-fun 6188  df-fv 6194  df-2nd 7501

This theorem is referenced by:  op2ndd  7511  op2ndg  7513  2ndval2  7518  fo2ndres  7527  opreuopreu  7545  eloprabi  7568  fo2ndf  7621  f1o2ndf1  7622  seqomlem1  7888  seqomlem2  7889  xpmapenlem  8479  fseqenlem2  9244  axdc4lem  9674  iunfo  9758  archnq  10199  om2uzrdg  13138  uzrdgsuci  13142  fsum2dlem  14984  fprod2dlem  15193  ruclem8  15449  ruclem11  15452  eucalglt  15784  idfu2nd  17018  idfucl  17022  cofu2nd  17026  cofucl  17029  xpccatid  17309  prf2nd  17326  curf2ndf  17368  yonedalem22  17399  gaid  18213  2ndcctbss  21783  upxp  21951  uptx  21953  txkgen  21980  cnheiborlem  23277  ovollb2lem  23808  ovolctb  23810  ovoliunlem2  23823  ovolshftlem1  23829  ovolscalem1  23833  ovolicc1  23836  addsqnreup  25737  2sqreuop  25756  2sqreuopnn  25757  2sqreuoplt  25758  2sqreuopltb  25759  2sqreuopnnlt  25760  2sqreuopnnltb  25761  wlkswwlksf1o  27381  clwlkclwwlkfoOLD  27535  clwlkclwwlkfo  27539  ex-2nd  28018  cnnvs  28250  cnnvnm  28251  h2hsm  28547  h2hnm  28548  hhsssm  28830  hhssnm  28831  aciunf1lem  30187  eulerpartlemgvv  31312  eulerpartlemgh  31314  msubff1  32356  msubvrs  32360  poimirlem17  34383  heiborlem7  34570  heiborlem8  34571  dvhvaddass  37711  dvhlveclem  37722  diblss  37784  pellexlem5  38860  pellex  38862  dvnprodlem1  41691  hoicvr  42291  hoicvrrex  42299  ovn0lem  42308  ovnhoilem1  42344  ovnlecvr2  42353  ovolval5lem2  42396