Theorem op1st 6405

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 6401	. 2
2		op1st.1	. . 3
3		op1st.2	. . 3
4	2, 3	op1sta 5397	. 2
5	1, 4	eqtri 2463	1

Syntax hints:  =wceq 1654  e.wcel 1728  cvv 2965  {csn 3841  <.cop 3844  U.cuni 4043  domcdm 4919  `cfv 5501  c1st 6397

This theorem is referenced by:  op1std  6407  op1stg  6409  1stval2  6414  fo1stres  6420  eloprabi  6463  algrflem  6505  xpmapenlem  7323  fseqenlem2  7957  archnq  8908  ruclem8  12887  idfu1st  14127  cofu1st  14131  xpccatid  14336  prf1st  14352  yonedalem21  14421  yonedalem22  14426  2ndcctbss  17569  upxp  17706  uptx  17708  cnheiborlem  19030  ovollb2lem  19435  ovolctb  19437  ovoliunlem2  19450  ovolshftlem1  19456  ovolscalem1  19460  ovolicc1  19463  ex-1st  21803  cnnvg  22220  cnnvs  22223  h2hva  22528  h2hsm  22529  hhssva  22810  hhsssm  22811  hhshsslem1  22818  eulerpartlemgvv  24762  eulerpartlemgh  24764  br1steq  25502  filnetlem3  26520  heiborlem8  26638  pellexlem5  27075  pellex  27077  dvhvaddass  32135  dvhlveclem  32146  diblss  32208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4364  ax-nul 4372  ax-pow 4416  ax-pr 4442  ax-un 4742

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-sbc 3171  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3766  df-sn 3847  df-pr 3848  df-op 3850  df-uni 4044  df-br 4244  df-opab 4302  df-mpt 4303  df-id 4539  df-xp 4925  df-rel 4926  df-cnv 4927  df-co 4928  df-dm 4929  df-rn 4930  df-iota 5464  df-fun 5503  df-fv 5509  df-1st 6399