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

Theorem op1st 6212
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 6208 . 2  |-  ( 1st `  <. A ,  B >. )  =  U. dom  {
<. A ,  B >. }
2 op1st.1 . . 3  |-  A  e. 
_V
3 op1st.2 . . 3  |-  B  e. 
_V
42, 3op1sta 5233 . 2  |-  U. dom  {
<. A ,  B >. }  =  A
51, 4eqtri 2378 1  |-  ( 1st `  <. A ,  B >. )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1642    e. wcel 1710   _Vcvv 2864   {csn 3716   <.cop 3719   U.cuni 3906   dom cdm 4768   ` cfv 5334   1stc1st 6204
This theorem is referenced by:  op1std  6214  op1stg  6216  1stval2  6221  fo1stres  6227  eloprabi  6270  algrflem  6308  xpmapenlem  7113  fseqenlem2  7739  archnq  8691  ruclem8  12606  idfu1st  13846  cofu1st  13850  xpccatid  14055  prf1st  14071  yonedalem21  14140  yonedalem22  14145  2ndcctbss  17281  upxp  17417  uptx  17419  cnheiborlem  18550  ovollb2lem  18945  ovolctb  18947  ovoliunlem2  18960  ovolshftlem1  18966  ovolscalem1  18970  ovolicc1  18973  ex-1st  20937  cnnvg  21354  cnnvs  21357  h2hva  21662  h2hsm  21663  hhssva  21944  hhsssm  21945  hhshsslem1  21952  br1steq  24688  filnetlem3  25653  heiborlem8  25865  pellexlem5  26241  pellex  26243  dvhvaddass  31339  dvhlveclem  31350  diblss  31412
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-mpt 4158  df-id 4388  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-iota 5298  df-fun 5336  df-fv 5342  df-1st 6206
  Copyright terms: Public domain W3C validator