ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  op2nd Unicode version

Theorem op2nd 6110
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
StepHypRef Expression
1 op1st.1 . . . 4  |-  A  e. 
_V
2 op1st.2 . . . 4  |-  B  e. 
_V
3 opexg 4203 . . . 4  |-  ( ( A  e.  _V  /\  B  e.  _V )  -> 
<. A ,  B >.  e. 
_V )
41, 2, 3mp2an 423 . . 3  |-  <. A ,  B >.  e.  _V
5 2ndvalg 6106 . . 3  |-  ( <. A ,  B >.  e. 
_V  ->  ( 2nd `  <. A ,  B >. )  =  U. ran  { <. A ,  B >. } )
64, 5ax-mp 5 . 2  |-  ( 2nd `  <. A ,  B >. )  =  U. ran  {
<. A ,  B >. }
71, 2op2nda 5085 . 2  |-  U. ran  {
<. A ,  B >. }  =  B
86, 7eqtri 2185 1  |-  ( 2nd `  <. A ,  B >. )  =  B
Colors of variables: wff set class
Syntax hints:    = wceq 1342    e. wcel 2135   _Vcvv 2724   {csn 3573   <.cop 3576   U.cuni 3786   ran crn 4602   ` cfv 5185   2ndc2nd 6102
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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4097  ax-pow 4150  ax-pr 4184  ax-un 4408
This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2726  df-sbc 2950  df-un 3118  df-in 3120  df-ss 3127  df-pw 3558  df-sn 3579  df-pr 3580  df-op 3582  df-uni 3787  df-br 3980  df-opab 4041  df-mpt 4042  df-id 4268  df-xp 4607  df-rel 4608  df-cnv 4609  df-co 4610  df-dm 4611  df-rn 4612  df-iota 5150  df-fun 5187  df-fv 5193  df-2nd 6104
This theorem is referenced by:  op2ndd  6112  op2ndg  6114  2ndval2  6119  fo2ndresm  6125  eloprabi  6159  fo2ndf  6189  f1o2ndf1  6190  xpmapenlem  6809  genpelvu  7448  nqprl  7486  1pru  7491  addnqprlemru  7493  addnqprlemfl  7494  addnqprlemfu  7495  mulnqprlemru  7509  mulnqprlemfl  7510  mulnqprlemfu  7511  ltnqpr  7528  ltnqpri  7529  ltexprlemelu  7534  recexprlemelu  7558  cauappcvgprlemm  7580  cauappcvgprlemopu  7583  cauappcvgprlemupu  7584  cauappcvgprlemdisj  7586  cauappcvgprlemloc  7587  cauappcvgprlemladdfu  7589  cauappcvgprlemladdru  7591  cauappcvgprlemladdrl  7592  cauappcvgprlem2  7595  caucvgprlemm  7603  caucvgprlemopu  7606  caucvgprlemupu  7607  caucvgprlemdisj  7609  caucvgprlemloc  7610  caucvgprlemladdfu  7612  caucvgprlem2  7615  caucvgprprlemelu  7621  caucvgprprlemmu  7630  caucvgprprlemexbt  7641  caucvgprprlem2  7645  suplocexprlemloc  7656  fsum2dlemstep  11369  fprod2dlemstep  11557  ctiunctlemfo  12366
  Copyright terms: Public domain W3C validator