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

Theorem op1stg 6786
Description: Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
Assertion
Ref Expression
op1stg  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( 1st `  <. A ,  B >. )  =  A )

Proof of Theorem op1stg
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 4206 . . . 4  |-  ( x  =  A  ->  <. x ,  y >.  =  <. A ,  y >. )
21fveq2d 5861 . . 3  |-  ( x  =  A  ->  ( 1st `  <. x ,  y
>. )  =  ( 1st `  <. A ,  y
>. ) )
3 id 22 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2482 . 2  |-  ( x  =  A  ->  (
( 1st `  <. x ,  y >. )  =  x  <->  ( 1st `  <. A ,  y >. )  =  A ) )
5 opeq2 4207 . . . 4  |-  ( y  =  B  ->  <. A , 
y >.  =  <. A ,  B >. )
65fveq2d 5861 . . 3  |-  ( y  =  B  ->  ( 1st `  <. A ,  y
>. )  =  ( 1st `  <. A ,  B >. ) )
76eqeq1d 2462 . 2  |-  ( y  =  B  ->  (
( 1st `  <. A ,  y >. )  =  A  <->  ( 1st `  <. A ,  B >. )  =  A ) )
8 vex 3109 . . 3  |-  x  e. 
_V
9 vex 3109 . . 3  |-  y  e. 
_V
108, 9op1st 6782 . 2  |-  ( 1st `  <. x ,  y
>. )  =  x
114, 7, 10vtocl2g 3168 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( 1st `  <. A ,  B >. )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762   <.cop 4026   ` cfv 5579   1stc1st 6772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-iota 5542  df-fun 5581  df-fv 5587  df-1st 6774
This theorem is referenced by:  ot1stg  6788  ot2ndg  6789  1stconst  6861  mpt2sn  6864  curry2  6868  mpt2xopn0yelv  6931  mpt2xopoveq  6937  xpmapenlem  7674  fpwwe  9013  addpipq  9304  mulpipq  9307  ordpipq  9309  swrdval  12594  ruclem1  13814  qnumdenbi  14125  oppccofval  14961  funcf2  15084  cofuval2  15103  resfval2  15109  resf1st  15110  isnat  15163  fucco  15178  homadm  15214  setcco  15257  xpcco  15299  xpchom2  15302  xpcco2  15303  evlf2  15334  curfval  15339  curf1cl  15344  uncf1  15352  uncf2  15353  diag11  15359  diag12  15360  diag2  15361  hof2fval  15371  yonedalem21  15389  yonedalem22  15394  mvmulfval  18804  imasdsf1olem  20604  ovolicc1  21655  ioombl1lem3  21698  ioombl1lem4  21699  brcgr  23872  nbgraop  24085  rngoablo2  25086  vcoprne  25134  fgreu  27171  fvtransport  29245  gordopval  31793  bj-inftyexpiinv  33558  bj-finsumval0  33610  dvhopvadd  35765  dvhopvsca  35774  dvhopaddN  35786  dvhopspN  35787
  Copyright terms: Public domain W3C validator