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

Theorem op2ndg 6579
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 4047 . . . 4  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
21fveq2d 5683 . . 3  |-  ( x  =  A  ->  ( 2nd `  <. x ,  y
>. )  =  ( 2nd `  <. A ,  y
>. ) )
32eqeq1d 2441 . 2  |-  ( x  =  A  ->  (
( 2nd `  <. x ,  y >. )  =  y  <->  ( 2nd `  <. A ,  y >. )  =  y ) )
4 opeq2 4048 . . . 4  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
54fveq2d 5683 . . 3  |-  ( y  =  B  ->  ( 2nd `  <. A ,  y
>. )  =  ( 2nd `  <. A ,  B >. ) )
6 id 22 . . 3  |-  ( y  =  B  ->  y  =  B )
75, 6eqeq12d 2447 . 2  |-  ( y  =  B  ->  (
( 2nd `  <. A ,  y >. )  =  y  <->  ( 2nd `  <. A ,  B >. )  =  B ) )
8 vex 2965 . . 3  |-  x  e. 
_V
9 vex 2965 . . 3  |-  y  e. 
_V
108, 9op2nd 6575 . 2  |-  ( 2nd `  <. x ,  y
>. )  =  y
113, 7, 10vtocl2g 3023 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( 2nd `  <. A ,  B >. )  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1362    e. wcel 1755   <.cop 3871   ` cfv 5406   2ndc2nd 6565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-iota 5369  df-fun 5408  df-fv 5414  df-2nd 6567
This theorem is referenced by:  ot2ndg  6581  ot3rdg  6582  2ndconst  6651  curry1  6653  xpmapenlem  7466  axdc4lem  8612  pinq  9083  addpipq  9093  mulpipq  9096  ordpipq  9098  swrdval  12296  ruclem1  13495  eucalg  13744  qnumdenbi  13804  comffval  14620  oppccofval  14637  funcf2  14760  cofuval2  14779  resfval2  14785  resf2nd  14787  funcres  14788  isnat  14839  fucco  14854  homacd  14891  setcco  14933  catcco  14951  xpcco  14975  xpchom2  14978  xpcco2  14979  evlf2  15010  curfval  15015  curf1cl  15020  uncf1  15028  uncf2  15029  hof2fval  15047  yonedalem21  15065  yonedalem22  15070  mvmulfval  18194  imasdsf1olem  19789  ovolicc1  20840  ioombl1lem3  20882  ioombl1lem4  20883  brcgr  22968  nbgraop  23157  vcoprne  23779  fvtransport  27909  mpt2sn  30565  lmod1zr  30741  bj-finsumval0  32156  dvhopvadd  34308  dvhopvsca  34317  dvhopaddN  34329  dvhopspN  34330
  Copyright terms: Public domain W3C validator