Theorem op2nd 7999

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3451  {csn 4584  ⟨cop 4590  ∪ cuni 4867  ran crn 5652  ‘cfv 6531  2^nd c2nd 7989

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fv 6539  df-2nd 7991

This theorem is used by:  op2ndd  8001  op2ndg  8003  2ndval2  8008  fo2ndres  8017  opreuopreu  8035  eloprabi  8063  fo2ndf  8121  f1o2ndf1  8122  seqomlem1  8444  seqomlem2  8445  xpmapenlem  9147  fseqenlem2  10085  axdc4lem  10514  iunfo  10604  archnq  11046  om2uzrdg  14079  uzrdgsuci  14083  fsum2dlem  15916  fprod2dlem  16127  ruclem8  16385  ruclem11  16388  eucalglt  16740  idfu2nd  18032  idfucl  18036  cofu2nd  18040  cofucl  18043  xpccatid  18342  prf2nd  18359  curf2ndf  18401  yonedalem22  18432  gaid  19493  2ndcctbss  23754  upxp  23922  uptx  23924  txkgen  23951  cnheiborlem  25255  ovollb2lem  25789  ovolctb  25791  ovoliunlem2  25804  ovolshftlem1  25810  ovolscalem1  25814  ovolicc1  25817  addsqnreup  27752  2sqreuop  27771  2sqreuopnn  27772  2sqreuoplt  27773  2sqreuopltb  27774  2sqreuopnnlt  27775  2sqreuopnnltb  27776  precsexlem2  28576  precsexlem5  28579  om2noseqrdg  28672  noseqrdgsuc  28676  wlkswwlksf1o  30450  clwlkclwwlkfo  30582  ex-2nd  31028  cnnvs  31264  cnnvnm  31265  h2hsm  31559  h2hnm  31560  hhsssm  31842  hhssnm  31843  2ndimaxp  33222  2ndresdju  33225  aciunf1lem  33238  gsumpart  33606  rlocf1  33817  fracfld  33852  eulerpartlemgvv  34991  eulerpartlemgh  34993  satfv0fvfmla0  36147  sategoelfvb  36153  prv1n  36165  msubff1  36290  msubvrs  36294  poimirlem17  38523  heiborlem7  38719  heiborlem8  38720  dvhvaddass  42122  dvhlveclem  42133  diblss  42195  aks6d1c3  43141  pellexlem5  43793  pellex  43795  dvnprodlem1  46900  hoicvr  47502  hoicvrrex  47510  ovn0lem  47519  ovnhoilem1  47555  ovnlecvr2  47564  ovolval5lem2  47607  gpg3kgrtriex  49131  pgnioedg1  49150  pgnioedg2  49151  pgnioedg3  49152  pgnioedg4  49153  pgnioedg5  49154  pgnbgreunbgrlem2lem1  49156  pgnbgreunbgrlem2lem2  49157  pgnbgreunbgrlem2lem3  49158  pgnbgreunbgrlem5lem1  49162  pgnbgreunbgrlem5lem2  49163  pgnbgreunbgrlem5lem3  49164  eloprab1st2nd  49922  swapf2fvala  50316  swapf2f1oaALT  50330  swapfcoa  50333  fuco21  50388  fucof21  50399  prcof2a  50441  prcof2  50442