Theorem op1st 6591

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 6585	. 2
2		op1st.1	. . 3
3		op1st.2	. . 3
4	2, 3	op1sta 5341	. 2
5	1, 4	eqtri 2509	1

Syntax hints:  =wceq 1670  e.wcel 1732  cvv 3015  {csn 3909  <.cop 3912  U.cuni 4117  domcdm 4862  `cfv 5438  c1st 6581

This theorem is referenced by:  op1std  6593  op1stg  6595  1stval2  6600  fo1stres  6606  eloprabi  6642  algrflem  6687  xpmapenlem  7439  fseqenlem2  8077  archnq  9028  ruclem8  13366  idfu1st  14630  cofu1st  14634  xpccatid  14839  prf1st  14855  yonedalem21  14924  yonedalem22  14929  2ndcctbss  18533  upxp  18670  uptx  18672  cnheiborlem  19994  ovollb2lem  20399  ovolctb  20401  ovoliunlem2  20414  ovolshftlem1  20420  ovolscalem1  20424  ovolicc1  20427  ex-1st  22773  cnnvg  23190  cnnvs  23193  h2hva  23498  h2hsm  23499  hhssva  23782  hhsssm  23783  hhshsslem1  23790  eulerpartlemgvv  25933  eulerpartlemgh  25935  br1steq  26737  filnetlem3  27781  heiborlem8  27899  pellexlem5  28322  pellex  28324  wlknwwlknsur  29525  wlkiswwlksur  29532  clwlkfoclwwlk  29699  dvhvaddass  33445  dvhlveclem  33456  diblss  33518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-sbc 3225  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-mpt 4378  df-id 4657  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-iota 5401  df-fun 5440  df-fv 5446  df-1st 6583