Theorem op2nd 7947

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  Vcvv 3432  {csn 4562  ⟨cop 4568  ∪ cuni 4845  ran crn 5626  ‘cfv 6492  2^nd c2nd 7937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fv 6500  df-2nd 7939

This theorem is referenced by:  op2ndd  7949  op2ndg  7951  2ndval2  7956  fo2ndres  7965  opreuopreu  7983  eloprabi  8012  fo2ndf  8067  f1o2ndf1  8068  seqomlem1  8386  seqomlem2  8387  xpmapenlem  9079  fseqenlem2  9945  axdc4lem  10375  iunfo  10459  archnq  10901  om2uzrdg  13916  uzrdgsuci  13920  fsum2dlem  15730  fprod2dlem  15943  ruclem8  16202  ruclem11  16205  eucalglt  16552  idfu2nd  17842  idfucl  17846  cofu2nd  17850  cofucl  17853  xpccatid  18152  prf2nd  18169  curf2ndf  18211  yonedalem22  18242  gaid  19272  2ndcctbss  23445  upxp  23613  uptx  23615  txkgen  23642  cnheiborlem  24946  ovollb2lem  25480  ovolctb  25482  ovoliunlem2  25495  ovolshftlem1  25501  ovolscalem1  25505  ovolicc1  25508  addsqnreup  27431  2sqreuop  27450  2sqreuopnn  27451  2sqreuoplt  27452  2sqreuopltb  27453  2sqreuopnnlt  27454  2sqreuopnnltb  27455  precsexlem2  28225  precsexlem5  28228  om2noseqrdg  28321  noseqrdgsuc  28325  wlkswwlksf1o  29972  clwlkclwwlkfo  30104  ex-2nd  30540  cnnvs  30776  cnnvnm  30777  h2hsm  31071  h2hnm  31072  hhsssm  31354  hhssnm  31355  2ndimaxp  32745  2ndresdju  32748  aciunf1lem  32761  gsumpart  33151  rlocf1  33361  fracfld  33399  eulerpartlemgvv  34567  eulerpartlemgh  34569  satfv0fvfmla0  35648  sategoelfvb  35654  prv1n  35666  msubff1  35791  msubvrs  35795  poimirlem17  38011  heiborlem7  38191  heiborlem8  38192  dvhvaddass  41596  dvhlveclem  41607  diblss  41669  aks6d1c3  42615  pellexlem5  43285  pellex  43287  dvnprodlem1  46396  hoicvr  46998  hoicvrrex  47006  ovn0lem  47015  ovnhoilem1  47051  ovnlecvr2  47060  ovolval5lem2  47103  gpg3kgrtriex  48587  pgnioedg1  48606  pgnioedg2  48607  pgnioedg3  48608  pgnioedg4  48609  pgnioedg5  48610  pgnbgreunbgrlem2lem1  48612  pgnbgreunbgrlem2lem2  48613  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem5lem1  48618  pgnbgreunbgrlem5lem2  48619  pgnbgreunbgrlem5lem3  48620  eloprab1st2nd  49365  swapf2fvala  49761  swapf2f1oaALT  49775  swapfcoa  49778  fuco21  49833  fucof21  49844  prcof2a  49886  prcof2  49887