Theorem op2nd 7999

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3453  {csn 4587  ⟨cop 4593  ∪ cuni 4870  ran crn 5660  ‘cfv 6537  2^nd c2nd 7989

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fv 6545  df-2nd 7991

This theorem is used by:  op2ndd  8001  op2ndg  8003  2ndval2  8008  fo2ndres  8017  opreuopreu  8035  eloprabi  8064  fo2ndf  8122  f1o2ndf1  8123  seqomlem1  8443  seqomlem2  8444  xpmapenlem  9146  fseqenlem2  10032  axdc4lem  10461  iunfo  10551  archnq  10993  om2uzrdg  14024  uzrdgsuci  14028  fsum2dlem  15860  fprod2dlem  16073  ruclem8  16331  ruclem11  16334  eucalglt  16681  idfu2nd  17972  idfucl  17976  cofu2nd  17980  cofucl  17983  xpccatid  18282  prf2nd  18299  curf2ndf  18341  yonedalem22  18372  gaid  19432  2ndcctbss  23687  upxp  23855  uptx  23857  txkgen  23884  cnheiborlem  25188  ovollb2lem  25722  ovolctb  25724  ovoliunlem2  25737  ovolshftlem1  25743  ovolscalem1  25747  ovolicc1  25750  addsqnreup  27687  2sqreuop  27706  2sqreuopnn  27707  2sqreuoplt  27708  2sqreuopltb  27709  2sqreuopnnlt  27710  2sqreuopnnltb  27711  precsexlem2  28481  precsexlem5  28484  om2noseqrdg  28577  noseqrdgsuc  28581  wlkswwlksf1o  30355  clwlkclwwlkfo  30487  ex-2nd  30933  cnnvs  31169  cnnvnm  31170  h2hsm  31464  h2hnm  31465  hhsssm  31747  hhssnm  31748  2ndimaxp  33127  2ndresdju  33130  aciunf1lem  33143  gsumpart  33511  rlocf1  33722  fracfld  33757  eulerpartlemgvv  34895  eulerpartlemgh  34897  satfv0fvfmla0  36000  sategoelfvb  36006  prv1n  36018  msubff1  36143  msubvrs  36147  poimirlem17  38394  heiborlem7  38575  heiborlem8  38576  dvhvaddass  41978  dvhlveclem  41989  diblss  42051  aks6d1c3  42997  pellexlem5  43682  pellex  43684  dvnprodlem1  46782  hoicvr  47384  hoicvrrex  47392  ovn0lem  47401  ovnhoilem1  47437  ovnlecvr2  47446  ovolval5lem2  47489  gpg3kgrtriex  49013  pgnioedg1  49032  pgnioedg2  49033  pgnioedg3  49034  pgnioedg4  49035  pgnioedg5  49036  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem5lem1  49044  pgnbgreunbgrlem5lem2  49045  pgnbgreunbgrlem5lem3  49046  eloprab1st2nd  49804  swapf2fvala  50198  swapf2f1oaALT  50212  swapfcoa  50215  fuco21  50270  fucof21  50281  prcof2a  50323  prcof2  50324