Theorem op1st 7934

Description: Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)

Hypotheses

Ref	Expression
op1st.1	⊢ 𝐴 ∈ V
op1st.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
op1st	⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴

Proof of Theorem op1st

Step	Hyp	Ref	Expression
1		1stval 7928	. 2 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = ∪ dom {⟨𝐴, 𝐵⟩}
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op1sta 6182	. 2 ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
5	1, 4	eqtri 2759	1 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2106  Vcvv 3446  {csn 4591  ⟨cop 4597  ∪ cuni 4870  dom cdm 5638  ‘cfv 6501  1^st c1st 7924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6453  df-fun 6503  df-fv 6509  df-1st 7926

This theorem is referenced by:  op1std  7936  op1stg  7938  1stval2  7943  fo1stres  7952  opreuopreu  7971  eloprabi  8000  xpmapenlem  9095  fseqenlem2  9970  archnq  10925  ruclem8  16130  idfu1st  17779  cofu1st  17783  xpccatid  18090  prf1st  18106  yonedalem21  18176  yonedalem22  18181  2ndcctbss  22843  upxp  23011  uptx  23013  cnheiborlem  24354  ovollb2lem  24889  ovolctb  24891  ovoliunlem2  24904  ovolshftlem1  24910  ovolscalem1  24914  ovolicc1  24917  addsqnreup  26828  2sqreuop  26847  2sqreuopnn  26848  2sqreuoplt  26849  2sqreuopltb  26850  2sqreuopnnlt  26851  2sqreuopnnltb  26852  ex-1st  29451  cnnvg  29683  cnnvs  29685  h2hva  29979  h2hsm  29980  hhssva  30262  hhsssm  30263  hhshsslem1  30272  gsumhashmul  31968  eulerpartlemgvv  33065  eulerpartlemgh  33067  satfv0fvfmla0  34094  filnetlem3  34928  poimirlem17  36168  heiborlem8  36350  dvhvaddass  39633  dvhlveclem  39644  diblss  39706  pellexlem5  41214  pellex  41216  dvnprodlem1  44307  hoicvr  44909  hoicvrrex  44917  ovn0lem  44926  ovnhoilem1  44962  thincciso  47189