Theorem op2nd 8037

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  Vcvv 3454  {csn 4588  ⟨cop 4838  ∪ cuni 4870  ran crn 5657  ‘cfv 6561  2^nd c2nd 8027

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396  ax-un 7778

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-iota 6515  df-fun 6563  df-fv 6569  df-2nd 8029

This theorem is used by:  op2ndd  8039  op2ndg  8041  2ndval2  8046  fo2ndres  8055  opreuopreu  8073  eloprabi  8102  fo2ndf  8162  f1o2ndf1  8163  seqomlem1  8491  seqomlem2  8492  xpmapenlem  9194  fseqenlem2  10134  axdc4lem  10563  iunfo  10653  archnq  11095  om2uzrdg  14129  uzrdgsuci  14133  fsum2dlem  15968  fprod2dlem  16179  ruclem8  16437  ruclem11  16440  eucalglt  16792  idfu2nd  18084  idfucl  18088  cofu2nd  18092  cofucl  18095  xpccatid  18394  prf2nd  18411  curf2ndf  18453  yonedalem22  18484  gaid  19546  2ndcctbss  23807  upxp  23975  uptx  23977  txkgen  24004  cnheiborlem  25308  ovollb2lem  25842  ovolctb  25844  ovoliunlem2  25857  ovolshftlem1  25863  ovolscalem1  25867  ovolicc1  25870  addsqnreup  27803  2sqreuop  27822  2sqreuopnn  27823  2sqreuoplt  27824  2sqreuopltb  27825  2sqreuopnnlt  27826  2sqreuopnnltb  27827  precsexlem2  28627  precsexlem5  28630  om2noseqrdg  28723  noseqrdgsuc  28727  wlkswwlksf1o  30501  clwlkclwwlkfo  30633  ex-2nd  31079  cnnvs  31315  cnnvnm  31316  h2hsm  31610  h2hnm  31611  hhsssm  31893  hhssnm  31894  2ndimaxp  33315  2ndresdju  33318  aciunf1lem  33331  gsumpart  33700  rlocf1  33911  fracfld  33954  eulerpartlemgvv  35091  eulerpartlemgh  35093  satfv0fvfmla0  36358  sategoelfvb  36364  prv1n  36376  msubff1  36501  msubvrs  36505  poimirlem17  38760  heiborlem7  38954  heiborlem8  38955  dvhvaddass  42357  dvhlveclem  42368  diblss  42430  aks6d1c3  43376  pellexlem5  44044  pellex  44046  dvnprodlem1  47171  hoicvr  47773  hoicvrrex  47781  ovn0lem  47790  ovnhoilem1  47826  ovnlecvr2  47835  ovolval5lem2  47878  gpg3kgrtriex  49402  pgnioedg1  49421  pgnioedg2  49422  pgnioedg3  49423  pgnioedg4  49424  pgnioedg5  49425  pgnbgreunbgrlem2lem1  49427  pgnbgreunbgrlem2lem2  49428  pgnbgreunbgrlem2lem3  49429  pgnbgreunbgrlem5lem1  49433  pgnbgreunbgrlem5lem2  49434  pgnbgreunbgrlem5lem3  49435  eloprab1st2nd  50194  swapf2fvala  50601  swapf2f1oaALT  50615  swapfcoa  50618  fuco21  50673  fucof21  50684  prcof2a  50739  prcof2  50740