Theorem op2nd 6246

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 4280	. . . 4 |- ( ( A e. _V /\ B e. _V ) -> <. A , B >. e. _V )
4	1, 2, 3	mp2an 426	. . 3 |- <. A , B >. e. _V
5		2ndvalg 6242	. . 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 5176	. 2 |- U. ran { <. A , B >. } = B
8	6, 7	eqtri 2227	1 |- ( 2nd ` <. A , B >. ) = B

Syntax hints:   = wceq 1373   e. wcel 2177   _Vcvv 2773   {csn 3638   <.cop 3641   U.cuni 3856   ran crn 4684   ` cfv 5280   2ndc2nd 6238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261  ax-un 4488

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-sbc 3003  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-opab 4114  df-mpt 4115  df-id 4348  df-xp 4689  df-rel 4690  df-cnv 4691  df-co 4692  df-dm 4693  df-rn 4694  df-iota 5241  df-fun 5282  df-fv 5288  df-2nd 6240

This theorem is referenced by:  op2ndd  6248  op2ndg  6250  2ndval2  6255  fo2ndresm  6261  eloprabi  6295  fo2ndf  6326  f1o2ndf1  6327  xpmapenlem  6961  genpelvu  7646  nqprl  7684  1pru  7689  addnqprlemru  7691  addnqprlemfl  7692  addnqprlemfu  7693  mulnqprlemru  7707  mulnqprlemfl  7708  mulnqprlemfu  7709  ltnqpr  7726  ltnqpri  7727  ltexprlemelu  7732  recexprlemelu  7756  cauappcvgprlemm  7778  cauappcvgprlemopu  7781  cauappcvgprlemupu  7782  cauappcvgprlemdisj  7784  cauappcvgprlemloc  7785  cauappcvgprlemladdfu  7787  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  cauappcvgprlem2  7793  caucvgprlemm  7801  caucvgprlemopu  7804  caucvgprlemupu  7805  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprlemladdfu  7810  caucvgprlem2  7813  caucvgprprlemelu  7819  caucvgprprlemmu  7828  caucvgprprlemexbt  7839  caucvgprprlem2  7843  suplocexprlemloc  7854  fsum2dlemstep  11820  fprod2dlemstep  12008  ctiunctlemfo  12885