Theorem op2nd 7980

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3450  {csn 4592  ⟨cop 4598  ∪ cuni 4874  ran crn 5642  ‘cfv 6514  2^nd c2nd 7970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-2nd 7972

This theorem is referenced by:  op2ndd  7982  op2ndg  7984  2ndval2  7989  fo2ndres  7998  opreuopreu  8016  eloprabi  8045  fo2ndf  8103  f1o2ndf1  8104  seqomlem1  8421  seqomlem2  8422  xpmapenlem  9114  fseqenlem2  9985  axdc4lem  10415  iunfo  10499  archnq  10940  om2uzrdg  13928  uzrdgsuci  13932  fsum2dlem  15743  fprod2dlem  15953  ruclem8  16212  ruclem11  16215  eucalglt  16562  idfu2nd  17846  idfucl  17850  cofu2nd  17854  cofucl  17857  xpccatid  18156  prf2nd  18173  curf2ndf  18215  yonedalem22  18246  gaid  19238  2ndcctbss  23349  upxp  23517  uptx  23519  txkgen  23546  cnheiborlem  24860  ovollb2lem  25396  ovolctb  25398  ovoliunlem2  25411  ovolshftlem1  25417  ovolscalem1  25421  ovolicc1  25424  addsqnreup  27361  2sqreuop  27380  2sqreuopnn  27381  2sqreuoplt  27382  2sqreuopltb  27383  2sqreuopnnlt  27384  2sqreuopnnltb  27385  precsexlem2  28117  precsexlem5  28120  om2noseqrdg  28205  noseqrdgsuc  28209  wlkswwlksf1o  29816  clwlkclwwlkfo  29945  ex-2nd  30381  cnnvs  30616  cnnvnm  30617  h2hsm  30911  h2hnm  30912  hhsssm  31194  hhssnm  31195  2ndimaxp  32577  2ndresdju  32580  aciunf1lem  32593  gsumpart  33004  rlocf1  33231  fracfld  33265  eulerpartlemgvv  34374  eulerpartlemgh  34376  satfv0fvfmla0  35407  sategoelfvb  35413  prv1n  35425  msubff1  35550  msubvrs  35554  poimirlem17  37638  heiborlem7  37818  heiborlem8  37819  dvhvaddass  41098  dvhlveclem  41109  diblss  41171  aks6d1c3  42118  pellexlem5  42828  pellex  42830  dvnprodlem1  45951  hoicvr  46553  hoicvrrex  46561  ovn0lem  46570  ovnhoilem1  46606  ovnlecvr2  46615  ovolval5lem2  46658  gpg3kgrtriex  48084  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  eloprab1st2nd  48860  swapf2fvala  49257  swapf2f1oaALT  49271  swapfcoa  49274  fuco21  49329  fucof21  49340  prcof2a  49382  prcof2  49383