Theorem op2nd 7942

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3440  {csn 4580  ⟨cop 4586  ∪ cuni 4863  ran crn 5625  ‘cfv 6492  2^nd c2nd 7932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  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 7934

This theorem is referenced by:  op2ndd  7944  op2ndg  7946  2ndval2  7951  fo2ndres  7960  opreuopreu  7978  eloprabi  8007  fo2ndf  8063  f1o2ndf1  8064  seqomlem1  8381  seqomlem2  8382  xpmapenlem  9072  fseqenlem2  9935  axdc4lem  10365  iunfo  10449  archnq  10891  om2uzrdg  13879  uzrdgsuci  13883  fsum2dlem  15693  fprod2dlem  15903  ruclem8  16162  ruclem11  16165  eucalglt  16512  idfu2nd  17801  idfucl  17805  cofu2nd  17809  cofucl  17812  xpccatid  18111  prf2nd  18128  curf2ndf  18170  yonedalem22  18201  gaid  19228  2ndcctbss  23399  upxp  23567  uptx  23569  txkgen  23596  cnheiborlem  24909  ovollb2lem  25445  ovolctb  25447  ovoliunlem2  25460  ovolshftlem1  25466  ovolscalem1  25470  ovolicc1  25473  addsqnreup  27410  2sqreuop  27429  2sqreuopnn  27430  2sqreuoplt  27431  2sqreuopltb  27432  2sqreuopnnlt  27433  2sqreuopnnltb  27434  precsexlem2  28204  precsexlem5  28207  om2noseqrdg  28300  noseqrdgsuc  28304  wlkswwlksf1o  29952  clwlkclwwlkfo  30084  ex-2nd  30520  cnnvs  30755  cnnvnm  30756  h2hsm  31050  h2hnm  31051  hhsssm  31333  hhssnm  31334  2ndimaxp  32724  2ndresdju  32727  aciunf1lem  32740  gsumpart  33146  rlocf1  33355  fracfld  33390  eulerpartlemgvv  34533  eulerpartlemgh  34535  satfv0fvfmla0  35607  sategoelfvb  35613  prv1n  35625  msubff1  35750  msubvrs  35754  poimirlem17  37834  heiborlem7  38014  heiborlem8  38015  dvhvaddass  41353  dvhlveclem  41364  diblss  41426  aks6d1c3  42373  pellexlem5  43071  pellex  43073  dvnprodlem1  46186  hoicvr  46788  hoicvrrex  46796  ovn0lem  46805  ovnhoilem1  46841  ovnlecvr2  46850  ovolval5lem2  46893  gpg3kgrtriex  48331  pgnioedg1  48350  pgnioedg2  48351  pgnioedg3  48352  pgnioedg4  48353  pgnioedg5  48354  pgnbgreunbgrlem2lem1  48356  pgnbgreunbgrlem2lem2  48357  pgnbgreunbgrlem2lem3  48358  pgnbgreunbgrlem5lem1  48362  pgnbgreunbgrlem5lem2  48363  pgnbgreunbgrlem5lem3  48364  eloprab1st2nd  49109  swapf2fvala  49505  swapf2f1oaALT  49519  swapfcoa  49522  fuco21  49577  fucof21  49588  prcof2a  49630  prcof2  49631