Theorem op1st 6546

Description: Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)

Hypotheses

Ref	Expression
op1st.1
op1st.2

Assertion

Ref	Expression
op1st

Proof of Theorem op1st

Step	Hyp	Ref	Expression
1		1stval 6540	. 2
2		op1st.1	. . 3
3		op1st.2	. . 3
4	2, 3	op1sta 5320	. 2
5	1, 4	eqtri 2501	1

Syntax hints:  =wceq 1662  e.wcel 1724  cvv 3006  {csn 3894  <.cop 3897  U.cuni 4101  domcdm 4844  `cfv 5417  c1st 6536

This theorem is referenced by:  op1std  6548  op1stg  6550  1stval2  6555  fo1stres  6561  eloprabi  6597  algrflem  6638  xpmapenlem  7386  fseqenlem2  8020  archnq  8971  ruclem8  13305  idfu1st  14567  cofu1st  14571  xpccatid  14776  prf1st  14792  yonedalem21  14861  yonedalem22  14866  2ndcctbss  18022  upxp  18159  uptx  18161  cnheiborlem  19483  ovollb2lem  19888  ovolctb  19890  ovoliunlem2  19903  ovolshftlem1  19909  ovolscalem1  19913  ovolicc1  19916  ex-1st  22261  cnnvg  22678  cnnvs  22681  h2hva  22986  h2hsm  22987  hhssva  23270  hhsssm  23271  hhshsslem1  23278  eulerpartlemgvv  25424  eulerpartlemgh  25426  br1steq  26228  filnetlem3  27272  heiborlem8  27390  pellexlem5  27825  pellex  27827  wlknwwlknsur  29203  wlkiswwlksur  29210  clwlkfoclwwlk  29377  dvhvaddass  33168  dvhlveclem  33179  diblss  33241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3008  df-sbc 3213  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-if 3813  df-sn 3900  df-pr 3901  df-op 3903  df-uni 4102  df-br 4303  df-opab 4361  df-mpt 4362  df-id 4639  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-iota 5380  df-fun 5419  df-fv 5425  df-1st 6538