Theorem op2nd 7944

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3430  {csn 4568  ⟨cop 4574  ∪ cuni 4851  ran crn 5625  ‘cfv 6492  2^nd c2nd 7934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-2nd 7936

This theorem is referenced by:  op2ndd  7946  op2ndg  7948  2ndval2  7953  fo2ndres  7962  opreuopreu  7980  eloprabi  8009  fo2ndf  8064  f1o2ndf1  8065  seqomlem1  8382  seqomlem2  8383  xpmapenlem  9075  fseqenlem2  9938  axdc4lem  10368  iunfo  10452  archnq  10894  om2uzrdg  13909  uzrdgsuci  13913  fsum2dlem  15723  fprod2dlem  15936  ruclem8  16195  ruclem11  16198  eucalglt  16545  idfu2nd  17835  idfucl  17839  cofu2nd  17843  cofucl  17846  xpccatid  18145  prf2nd  18162  curf2ndf  18204  yonedalem22  18235  gaid  19265  2ndcctbss  23430  upxp  23598  uptx  23600  txkgen  23627  cnheiborlem  24931  ovollb2lem  25465  ovolctb  25467  ovoliunlem2  25480  ovolshftlem1  25486  ovolscalem1  25490  ovolicc1  25493  addsqnreup  27420  2sqreuop  27439  2sqreuopnn  27440  2sqreuoplt  27441  2sqreuopltb  27442  2sqreuopnnlt  27443  2sqreuopnnltb  27444  precsexlem2  28214  precsexlem5  28217  om2noseqrdg  28310  noseqrdgsuc  28314  wlkswwlksf1o  29962  clwlkclwwlkfo  30094  ex-2nd  30530  cnnvs  30766  cnnvnm  30767  h2hsm  31061  h2hnm  31062  hhsssm  31344  hhssnm  31345  2ndimaxp  32734  2ndresdju  32737  aciunf1lem  32750  gsumpart  33139  rlocf1  33349  fracfld  33384  eulerpartlemgvv  34536  eulerpartlemgh  34538  satfv0fvfmla0  35611  sategoelfvb  35617  prv1n  35629  msubff1  35754  msubvrs  35758  poimirlem17  37972  heiborlem7  38152  heiborlem8  38153  dvhvaddass  41557  dvhlveclem  41568  diblss  41630  aks6d1c3  42576  pellexlem5  43279  pellex  43281  dvnprodlem1  46392  hoicvr  46994  hoicvrrex  47002  ovn0lem  47011  ovnhoilem1  47047  ovnlecvr2  47056  ovolval5lem2  47099  gpg3kgrtriex  48577  pgnioedg1  48596  pgnioedg2  48597  pgnioedg3  48598  pgnioedg4  48599  pgnioedg5  48600  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem5lem1  48608  pgnbgreunbgrlem5lem2  48609  pgnbgreunbgrlem5lem3  48610  eloprab1st2nd  49355  swapf2fvala  49751  swapf2f1oaALT  49765  swapfcoa  49768  fuco21  49823  fucof21  49834  prcof2a  49876  prcof2  49877