Theorem op1st 6803

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

Step	Hyp	Ref	Expression
1		1stval 6797	. 2 |- ( 1st ` <. A , B >. ) = U. dom { <. A , B >. }
2		op1st.1	. . 3 |- A e. _V
3		op1st.2	. . 3 |- B e. _V
4	2, 3	op1sta 5496	. 2 |- U. dom { <. A , B >. } = A
5	1, 4	eqtri 2496	1 |- ( 1st ` <. A , B >. ) = A

Syntax hints:   = wceq 1379   e. wcel 1767   _Vcvv 3118   {csn 4033   <.cop 4039   U.cuni 4251   dom cdm 5005   ` cfv 5594   1stc1st 6793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-iota 5557  df-fun 5596  df-fv 5602  df-1st 6795

This theorem is referenced by:  op1std  6805  op1stg  6807  1stval2  6812  fo1stres  6819  eloprabi  6857  algrflem  6904  xpmapenlem  7696  fseqenlem2  8418  archnq  9370  ruclem8  13848  idfu1st  15123  cofu1st  15127  xpccatid  15332  prf1st  15348  yonedalem21  15417  yonedalem22  15422  2ndcctbss  19824  upxp  19992  uptx  19994  cnheiborlem  21322  ovollb2lem  21767  ovolctb  21769  ovoliunlem2  21782  ovolshftlem1  21788  ovolscalem1  21792  ovolicc1  21795  usgraexmplvtx  24216  wlknwwlknsur  24526  wlkiswwlksur  24533  clwlkfoclwwlk  24659  ex-1st  24980  cnnvg  25397  cnnvs  25400  h2hva  25705  h2hsm  25706  hhssva  25989  hhsssm  25990  hhshsslem1  25997  eulerpartlemgvv  28131  eulerpartlemgh  28133  br1steq  29122  filnetlem3  30116  heiborlem8  30232  pellexlem5  30688  pellex  30690  usgfis  32227  usgfisALT  32231  dvhvaddass  36250  dvhlveclem  36261  diblss  36323