Theorem op1st 6798

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

Syntax hints:   = wceq 1443   e. wcel 1886   _Vcvv 3044   {csn 3967   <.cop 3973   U.cuni 4197   dom cdm 4833   ` cfv 5581   1stc1st 6788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-iota 5545  df-fun 5583  df-fv 5589  df-1st 6790

This theorem is referenced by:  op1std  6800  op1stg  6802  1stval2  6807  fo1stres  6814  eloprabi  6852  algrflem  6902  xpmapenlem  7736  fseqenlem2  8453  archnq  9402  ruclem8  14282  idfu1st  15777  cofu1st  15781  xpccatid  16066  prf1st  16082  yonedalem21  16151  yonedalem22  16156  2ndcctbss  20463  upxp  20631  uptx  20633  cnheiborlem  21975  ovollb2lem  22434  ovolctb  22436  ovoliunlem2  22449  ovolshftlem1  22455  ovolscalem1  22459  ovolicc1  22462  usgraexmplvtx  25123  wlknwwlknsur  25433  wlkiswwlksur  25440  clwlkfoclwwlk  25566  ex-1st  25887  cnnvg  26302  cnnvs  26305  h2hva  26620  h2hsm  26621  hhssva  26903  hhsssm  26904  hhshsslem1  26911  eulerpartlemgvv  29202  eulerpartlemgh  29204  br1steq  30407  filnetlem3  31029  poimirlem17  31950  heiborlem8  32143  dvhvaddass  34659  dvhlveclem  34670  diblss  34732  pellexlem5  35671  pellex  35673  dvnprodlem1  37815  hoicvr  38364  hoicvrrex  38372  ovn0lem  38381  ovnhoilem1  38417  vtxvalsnop  39127  usgfis  39745  usgfisALT  39749