Theorem op2nd 6385

Description: Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)

Hypotheses

Ref	Expression
op1st.1	|- A e. _V
op1st.2	|- B e. _V

Assertion

Ref	Expression
op2nd	|- ( 2nd ` <. A , B >. ) = B

Proof of Theorem op2nd

Step	Hyp	Ref	Expression
1		op1st.1	. . . 4 |- A e. _V
2		op1st.2	. . . 4 |- B e. _V
3		opexg 4370	. . . 4 |- ( ( A e. _V /\ B e. _V ) -> <. A , B >. e. _V )
4	1, 2, 3	mp2an 430	. . 3 |- <. A , B >. e. _V
5		2ndvalg 6381	. . 3 |- ( <. A , B >. e. _V -> ( 2nd ` <. A , B >. ) = U. ran { <. A , B >. } )
6	4, 5	ax-mp 5	. 2 |- ( 2nd ` <. A , B >. ) = U. ran { <. A , B >. }
7	1, 2	op2nda 5275	. 2 |- U. ran { <. A , B >. } = B
8	6, 7	eqtri 2259	1 |- ( 2nd ` <. A , B >. ) = B

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209   _Vcvv 2821   {csn 3709   <.cop 3712   U.cuni 3935   ran crn 4777   ` cfv 5380   2ndc2nd 6377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-iota 5340  df-fun 5382  df-fv 5388  df-2nd 6379

This theorem is used by:  op2ndd  6387  op2ndg  6389  2ndval2  6394  fo2ndresm  6400  eloprabi  6436  fo2ndf  6467  f1o2ndf1  6468  xpmapenlem  7153  genpelvu  7886  nqprl  7924  1pru  7929  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  ltnqpr  7966  ltnqpri  7967  ltexprlemelu  7972  recexprlemelu  7996  cauappcvgprlemm  8018  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemelu  8059  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocexprlemloc  8094  fsum2dlemstep  12226  fprod2dlemstep  12414  ctiunctlemfo  13388