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

Theorem op1st 6130
Description: Extract the first 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
op1st  |-  ( 1st `  <. A ,  B >. )  =  A

Proof of Theorem op1st
StepHypRef Expression
1 1stval 6126 . 2  |-  ( 1st `  <. A ,  B >. )  =  U. dom  {
<. A ,  B >. }
2 op1st.1 . . 3  |-  A  e. 
_V
3 op1st.2 . . 3  |-  B  e. 
_V
42, 3op1sta 5156 . 2  |-  U. dom  {
<. A ,  B >. }  =  A
51, 4eqtri 2305 1  |-  ( 1st `  <. A ,  B >. )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1625    e. wcel 1686   _Vcvv 2790   {csn 3642   <.cop 3645   U.cuni 3829   dom cdm 4691   ` cfv 5257   1stc1st 6122
This theorem is referenced by:  op1std  6132  op1stg  6134  1stval2  6139  fo1stres  6145  eloprabi  6188  algrflem  6226  xpmapenlem  7030  fseqenlem2  7654  archnq  8606  ruclem8  12517  idfu1st  13755  cofu1st  13759  xpccatid  13964  prf1st  13980  yonedalem21  14049  yonedalem22  14054  2ndcctbss  17183  upxp  17319  uptx  17321  cnheiborlem  18454  ovollb2lem  18849  ovolctb  18851  ovoliunlem2  18864  ovolshftlem1  18870  ovolscalem1  18874  ovolicc1  18877  ex-1st  20833  cnnvg  21248  cnnvs  21251  h2hva  21556  h2hsm  21557  hhssva  21838  hhsssm  21839  hhshsslem1  21846  br1steq  24132  prj1b  25090  mulveczer  25490  mulinvsca  25491  muldisc  25492  svli2  25495  cmp2morpdom  25975  cmp2morpcod  25976  filnetlem3  26340  heiborlem8  26553  pellexlem5  26929  pellex  26931  dvhvaddass  31360  dvhlveclem  31371  diblss  31433
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-iota 5221  df-fun 5259  df-fv 5265  df-1st 6124
  Copyright terms: Public domain W3C validator