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

Theorem op2ndg 6730
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 4144 . . . 4  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
21fveq2d 5791 . . 3  |-  ( x  =  A  ->  ( 2nd `  <. x ,  y
>. )  =  ( 2nd `  <. A ,  y
>. ) )
32eqeq1d 2394 . 2  |-  ( x  =  A  ->  (
( 2nd `  <. x ,  y >. )  =  y  <->  ( 2nd `  <. A ,  y >. )  =  y ) )
4 opeq2 4145 . . . 4  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
54fveq2d 5791 . . 3  |-  ( y  =  B  ->  ( 2nd `  <. A ,  y
>. )  =  ( 2nd `  <. A ,  B >. ) )
6 id 22 . . 3  |-  ( y  =  B  ->  y  =  B )
75, 6eqeq12d 2414 . 2  |-  ( y  =  B  ->  (
( 2nd `  <. A ,  y >. )  =  y  <->  ( 2nd `  <. A ,  B >. )  =  B ) )
8 vex 3050 . . 3  |-  x  e. 
_V
9 vex 3050 . . 3  |-  y  e. 
_V
108, 9op2nd 6726 . 2  |-  ( 2nd `  <. x ,  y
>. )  =  y
113, 7, 10vtocl2g 3109 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( 2nd `  <. A ,  B >. )  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399    e. wcel 1836   <.cop 3963   ` cfv 5509   2ndc2nd 6716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-iota 5473  df-fun 5511  df-fv 5517  df-2nd 6718
This theorem is referenced by:  ot2ndg  6732  ot3rdg  6733  2ndconst  6806  mpt2sn  6808  curry1  6809  xpmapenlem  7621  axdc4lem  8766  pinq  9234  addpipq  9244  mulpipq  9247  ordpipq  9249  swrdval  12572  ruclem1  13985  eucalg  14237  qnumdenbi  14298  comffval  15124  oppccofval  15141  funcf2  15293  cofuval2  15312  resfval2  15318  resf2nd  15320  funcres  15321  isnat  15372  fucco  15387  homacd  15456  setcco  15498  catcco  15516  estrcco  15535  xpcco  15588  xpchom2  15591  xpcco2  15592  evlf2  15623  curfval  15628  curf1cl  15633  uncf1  15641  uncf2  15642  hof2fval  15660  yonedalem21  15678  yonedalem22  15683  mvmulfval  19148  imasdsf1olem  20980  ovolicc1  22031  ioombl1lem3  22074  ioombl1lem4  22075  brcgr  24345  edgopval  24482  nbgraop  24565  nbgraopALT  24566  vcoprne  25610  fvtransport  29871  etransclem44  32262  gsizopval  32744  rngccoALTV  33031  ringccoALTV  33094  lmod1zr  33329  bj-elid3  34984  bj-finsumval0  35045  dvhopvadd  37268  dvhopvsca  37277  dvhopaddN  37289  dvhopspN  37290
  Copyright terms: Public domain W3C validator