Theorem op1st 6791

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

Syntax hints:   = wceq 1405   e. wcel 1842   _Vcvv 3058   {csn 3971   <.cop 3977   U.cuni 4190   dom cdm 4822   ` cfv 5568   1stc1st 6781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-iota 5532  df-fun 5570  df-fv 5576  df-1st 6783

This theorem is referenced by:  op1std  6793  op1stg  6795  1stval2  6800  fo1stres  6807  eloprabi  6845  algrflem  6892  xpmapenlem  7721  fseqenlem2  8437  archnq  9387  ruclem8  14177  idfu1st  15490  cofu1st  15494  xpccatid  15779  prf1st  15795  yonedalem21  15864  yonedalem22  15869  2ndcctbss  20246  upxp  20414  uptx  20416  cnheiborlem  21744  ovollb2lem  22189  ovolctb  22191  ovoliunlem2  22204  ovolshftlem1  22210  ovolscalem1  22214  ovolicc1  22217  usgraexmplvtx  24806  wlknwwlknsur  25116  wlkiswwlksur  25123  clwlkfoclwwlk  25249  ex-1st  25569  cnnvg  25983  cnnvs  25986  h2hva  26291  h2hsm  26292  hhssva  26575  hhsssm  26576  hhshsslem1  26583  eulerpartlemgvv  28807  eulerpartlemgh  28809  br1steq  29974  filnetlem3  30595  heiborlem8  31576  dvhvaddass  34097  dvhlveclem  34108  diblss  34170  pellexlem5  35110  pellex  35112  dvnprodlem1  37092  usgfis  38056  usgfisALT  38060