Theorem op2nd 6092

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		op1st.1	. . . 4 ⊢ 𝐴 ∈ V
2		op1st.2	. . . 4 ⊢ 𝐵 ∈ V
3		opexg 4188	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐴, 𝐵⟩ ∈ V)
4	1, 2, 3	mp2an 423	. . 3 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
5		2ndvalg 6088	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ V → (2nd ‘⟨𝐴, 𝐵⟩) = ∪ ran {⟨𝐴, 𝐵⟩})
6	4, 5	ax-mp 5	. 2 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = ∪ ran {⟨𝐴, 𝐵⟩}
7	1, 2	op2nda 5069	. 2 ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
8	6, 7	eqtri 2178	1 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵

Syntax hints:   = wceq 1335   ∈ wcel 2128  Vcvv 2712  {csn 3560  ⟨cop 3563  ∪ cuni 3772  ran crn 4586  ‘cfv 5169  2^nd c2nd 6084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-sbc 2938  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4253  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-iota 5134  df-fun 5171  df-fv 5177  df-2nd 6086

This theorem is referenced by:  op2ndd  6094  op2ndg  6096  2ndval2  6101  fo2ndresm  6107  eloprabi  6141  fo2ndf  6171  f1o2ndf1  6172  xpmapenlem  6791  genpelvu  7428  nqprl  7466  1pru  7471  addnqprlemru  7473  addnqprlemfl  7474  addnqprlemfu  7475  mulnqprlemru  7489  mulnqprlemfl  7490  mulnqprlemfu  7491  ltnqpr  7508  ltnqpri  7509  ltexprlemelu  7514  recexprlemelu  7538  cauappcvgprlemm  7560  cauappcvgprlemopu  7563  cauappcvgprlemupu  7564  cauappcvgprlemdisj  7566  cauappcvgprlemloc  7567  cauappcvgprlemladdfu  7569  cauappcvgprlemladdru  7571  cauappcvgprlemladdrl  7572  cauappcvgprlem2  7575  caucvgprlemm  7583  caucvgprlemopu  7586  caucvgprlemupu  7587  caucvgprlemdisj  7589  caucvgprlemloc  7590  caucvgprlemladdfu  7592  caucvgprlem2  7595  caucvgprprlemelu  7601  caucvgprprlemmu  7610  caucvgprprlemexbt  7621  caucvgprprlem2  7625  suplocexprlemloc  7636  fsum2dlemstep  11326  fprod2dlemstep  11514  ctiunctlemfo  12155