Theorem op2nd 8004

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  Vcvv 3458  {csn 4594  ⟨cop 4600  ∪ cuni 4877  ran crn 5667  ‘cfv 6543  2^nd c2nd 7994

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fv 6551  df-2nd 7996

This theorem is used by:  op2ndd  8006  op2ndg  8008  2ndval2  8013  fo2ndres  8022  opreuopreu  8040  eloprabi  8069  fo2ndf  8125  f1o2ndf1  8126  seqomlem1  8446  seqomlem2  8447  xpmapenlem  9142  fseqenlem2  10028  axdc4lem  10457  iunfo  10541  archnq  10983  om2uzrdg  14012  uzrdgsuci  14016  fsum2dlem  15847  fprod2dlem  16060  ruclem8  16318  ruclem11  16321  eucalglt  16668  idfu2nd  17959  idfucl  17963  cofu2nd  17967  cofucl  17970  xpccatid  18269  prf2nd  18286  curf2ndf  18328  yonedalem22  18359  gaid  19400  2ndcctbss  23649  upxp  23817  uptx  23819  txkgen  23846  cnheiborlem  25150  ovollb2lem  25684  ovolctb  25686  ovoliunlem2  25699  ovolshftlem1  25705  ovolscalem1  25709  ovolicc1  25712  addsqnreup  27644  2sqreuop  27663  2sqreuopnn  27664  2sqreuoplt  27665  2sqreuopltb  27666  2sqreuopnnlt  27667  2sqreuopnnltb  27668  precsexlem2  28438  precsexlem5  28441  om2noseqrdg  28534  noseqrdgsuc  28538  wlkswwlksf1o  30265  clwlkclwwlkfo  30397  ex-2nd  30833  cnnvs  31069  cnnvnm  31070  h2hsm  31364  h2hnm  31365  hhsssm  31647  hhssnm  31648  2ndimaxp  33028  2ndresdju  33031  aciunf1lem  33044  gsumpart  33414  rlocf1  33625  fracfld  33660  eulerpartlemgvv  34798  eulerpartlemgh  34800  satfv0fvfmla0  35926  sategoelfvb  35932  prv1n  35944  msubff1  36069  msubvrs  36073  poimirlem17  38329  heiborlem7  38509  heiborlem8  38510  dvhvaddass  41912  dvhlveclem  41923  diblss  41985  aks6d1c3  42931  pellexlem5  43601  pellex  43603  dvnprodlem1  46701  hoicvr  47303  hoicvrrex  47311  ovn0lem  47320  ovnhoilem1  47356  ovnlecvr2  47365  ovolval5lem2  47408  gpg3kgrtriex  48895  pgnioedg1  48914  pgnioedg2  48915  pgnioedg3  48916  pgnioedg4  48917  pgnioedg5  48918  pgnbgreunbgrlem2lem1  48920  pgnbgreunbgrlem2lem2  48921  pgnbgreunbgrlem2lem3  48922  pgnbgreunbgrlem5lem1  48926  pgnbgreunbgrlem5lem2  48927  pgnbgreunbgrlem5lem3  48928  eloprab1st2nd  49687  swapf2fvala  50083  swapf2f1oaALT  50097  swapfcoa  50100  fuco21  50155  fucof21  50166  prcof2a  50208  prcof2  50209