MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  op2ndg Structured version   Unicode version

Theorem op2ndg 6795
Description: Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
Assertion
Ref Expression
op2ndg  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( 2nd `  <. A ,  B >. )  =  B )

Proof of Theorem op2ndg
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 4199 . . . 4  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
21fveq2d 5857 . . 3  |-  ( x  =  A  ->  ( 2nd `  <. x ,  y
>. )  =  ( 2nd `  <. A ,  y
>. ) )
32eqeq1d 2443 . 2  |-  ( x  =  A  ->  (
( 2nd `  <. x ,  y >. )  =  y  <->  ( 2nd `  <. A ,  y >. )  =  y ) )
4 opeq2 4200 . . . 4  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
54fveq2d 5857 . . 3  |-  ( y  =  B  ->  ( 2nd `  <. A ,  y
>. )  =  ( 2nd `  <. A ,  B >. ) )
6 id 22 . . 3  |-  ( y  =  B  ->  y  =  B )
75, 6eqeq12d 2463 . 2  |-  ( y  =  B  ->  (
( 2nd `  <. A ,  y >. )  =  y  <->  ( 2nd `  <. A ,  B >. )  =  B ) )
8 vex 3096 . . 3  |-  x  e. 
_V
9 vex 3096 . . 3  |-  y  e. 
_V
108, 9op2nd 6791 . 2  |-  ( 2nd `  <. x ,  y
>. )  =  y
113, 7, 10vtocl2g 3155 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( 2nd `  <. A ,  B >. )  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1381    e. wcel 1802   <.cop 4017   ` cfv 5575   2ndc2nd 6781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-mpt 4494  df-id 4782  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-iota 5538  df-fun 5577  df-fv 5583  df-2nd 6783
This theorem is referenced by:  ot2ndg  6797  ot3rdg  6798  2ndconst  6871  mpt2sn  6873  curry1  6874  xpmapenlem  7683  axdc4lem  8835  pinq  9305  addpipq  9315  mulpipq  9318  ordpipq  9320  swrdval  12620  ruclem1  13838  eucalg  14090  qnumdenbi  14151  comffval  14968  oppccofval  14985  funcf2  15108  cofuval2  15127  resfval2  15133  resf2nd  15135  funcres  15136  isnat  15187  fucco  15202  homacd  15239  setcco  15281  catcco  15299  xpcco  15323  xpchom2  15326  xpcco2  15327  evlf2  15358  curfval  15363  curf1cl  15368  uncf1  15376  uncf2  15377  hof2fval  15395  yonedalem21  15413  yonedalem22  15418  mvmulfval  18914  imasdsf1olem  20746  ovolicc1  21797  ioombl1lem3  21840  ioombl1lem4  21841  brcgr  24072  edgopval  24209  nbgraop  24292  nbgraopALT  24293  vcoprne  25341  fvtransport  29654  gsizopval  32229  estrcco  32482  rngccoOLD  32533  ringccoOLD  32591  lmod1zr  32824  bj-finsumval0  34386  dvhopvadd  36543  dvhopvsca  36552  dvhopaddN  36564  dvhopspN  36565
  Copyright terms: Public domain W3C validator