Theorem op2nd 7936

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {csn 4575  ⟨cop 4581  ∪ cuni 4858  ran crn 5620  ‘cfv 6487  2^nd c2nd 7926

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6443  df-fun 6489  df-fv 6495  df-2nd 7928

This theorem is referenced by:  op2ndd  7938  op2ndg  7940  2ndval2  7945  fo2ndres  7954  opreuopreu  7972  eloprabi  8001  fo2ndf  8057  f1o2ndf1  8058  seqomlem1  8375  seqomlem2  8376  xpmapenlem  9063  fseqenlem2  9922  axdc4lem  10352  iunfo  10436  archnq  10877  om2uzrdg  13869  uzrdgsuci  13873  fsum2dlem  15683  fprod2dlem  15893  ruclem8  16152  ruclem11  16155  eucalglt  16502  idfu2nd  17790  idfucl  17794  cofu2nd  17798  cofucl  17801  xpccatid  18100  prf2nd  18117  curf2ndf  18159  yonedalem22  18190  gaid  19217  2ndcctbss  23376  upxp  23544  uptx  23546  txkgen  23573  cnheiborlem  24886  ovollb2lem  25422  ovolctb  25424  ovoliunlem2  25437  ovolshftlem1  25443  ovolscalem1  25447  ovolicc1  25450  addsqnreup  27387  2sqreuop  27406  2sqreuopnn  27407  2sqreuoplt  27408  2sqreuopltb  27409  2sqreuopnnlt  27410  2sqreuopnnltb  27411  precsexlem2  28152  precsexlem5  28155  om2noseqrdg  28240  noseqrdgsuc  28244  wlkswwlksf1o  29864  clwlkclwwlkfo  29996  ex-2nd  30432  cnnvs  30667  cnnvnm  30668  h2hsm  30962  h2hnm  30963  hhsssm  31245  hhssnm  31246  2ndimaxp  32635  2ndresdju  32638  aciunf1lem  32651  gsumpart  33044  rlocf1  33247  fracfld  33281  eulerpartlemgvv  34396  eulerpartlemgh  34398  satfv0fvfmla0  35464  sategoelfvb  35470  prv1n  35482  msubff1  35607  msubvrs  35611  poimirlem17  37683  heiborlem7  37863  heiborlem8  37864  dvhvaddass  41202  dvhlveclem  41213  diblss  41275  aks6d1c3  42222  pellexlem5  42931  pellex  42933  dvnprodlem1  46049  hoicvr  46651  hoicvrrex  46659  ovn0lem  46668  ovnhoilem1  46704  ovnlecvr2  46713  ovolval5lem2  46756  gpg3kgrtriex  48194  pgnioedg1  48213  pgnioedg2  48214  pgnioedg3  48215  pgnioedg4  48216  pgnioedg5  48217  pgnbgreunbgrlem2lem1  48219  pgnbgreunbgrlem2lem2  48220  pgnbgreunbgrlem2lem3  48221  pgnbgreunbgrlem5lem1  48225  pgnbgreunbgrlem5lem2  48226  pgnbgreunbgrlem5lem3  48227  eloprab1st2nd  48973  swapf2fvala  49370  swapf2f1oaALT  49384  swapfcoa  49387  fuco21  49442  fucof21  49453  prcof2a  49495  prcof2  49496