Theorem op1st 6584

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 6578	. 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 5320	. 2 |- U. dom { <. A , B >. } = A
5	1, 4	eqtri 2462	1 |- ( 1st ` <. A , B >. ) = A

Syntax hints:   = wceq 1369   e. wcel 1756   _Vcvv 2971   {csn 3876   <.cop 3882   U.cuni 4090   dom cdm 4839   ` cfv 5417   1stc1st 6574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pow 4469  ax-pr 4530  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-sbc 3186  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-opab 4350  df-mpt 4351  df-id 4635  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-iota 5380  df-fun 5419  df-fv 5425  df-1st 6576

This theorem is referenced by:  op1std  6586  op1stg  6588  1stval2  6593  fo1stres  6599  eloprabi  6635  algrflem  6680  xpmapenlem  7477  fseqenlem2  8194  archnq  9148  ruclem8  13518  idfu1st  14788  cofu1st  14792  xpccatid  14997  prf1st  15013  yonedalem21  15082  yonedalem22  15087  2ndcctbss  19058  upxp  19195  uptx  19197  cnheiborlem  20525  ovollb2lem  20970  ovolctb  20972  ovoliunlem2  20985  ovolshftlem1  20991  ovolscalem1  20995  ovolicc1  20998  ex-1st  23650  cnnvg  24067  cnnvs  24070  h2hva  24375  h2hsm  24376  hhssva  24659  hhsssm  24660  hhshsslem1  24667  eulerpartlemgvv  26758  eulerpartlemgh  26760  br1steq  27584  filnetlem3  28599  heiborlem8  28715  pellexlem5  29172  pellex  29174  wlknwwlknsur  30342  wlkiswwlksur  30349  clwlkfoclwwlk  30516  dvhvaddass  34740  dvhlveclem  34751  diblss  34813