Theorem op1st 7987

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 7981	. 2 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = ∪ dom {⟨𝐴, 𝐵⟩}
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op1sta 6225	. 2 ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
5	1, 4	eqtri 2758	1 ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2104  Vcvv 3472  {csn 4629  ⟨cop 4635  ∪ cuni 4909  dom cdm 5677  ‘cfv 6544  1^st c1st 7977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fv 6552  df-1st 7979

This theorem is referenced by:  op1std  7989  op1stg  7991  1stval2  7996  fo1stres  8005  opreuopreu  8024  eloprabi  8053  xpmapenlem  9148  fseqenlem2  10024  archnq  10979  ruclem8  16186  idfu1st  17835  cofu1st  17839  xpccatid  18146  prf1st  18162  yonedalem21  18232  yonedalem22  18237  2ndcctbss  23181  upxp  23349  uptx  23351  cnheiborlem  24702  ovollb2lem  25239  ovolctb  25241  ovoliunlem2  25254  ovolshftlem1  25260  ovolscalem1  25264  ovolicc1  25267  addsqnreup  27180  2sqreuop  27199  2sqreuopnn  27200  2sqreuoplt  27201  2sqreuopltb  27202  2sqreuopnnlt  27203  2sqreuopnnltb  27204  precsexlem1  27890  precsexlem4  27893  ex-1st  29962  cnnvg  30196  cnnvs  30198  h2hva  30492  h2hsm  30493  hhssva  30775  hhsssm  30776  hhshsslem1  30785  gsumhashmul  32476  eulerpartlemgvv  33671  eulerpartlemgh  33673  satfv0fvfmla0  34700  filnetlem3  35570  poimirlem17  36810  heiborlem8  36991  dvhvaddass  40273  dvhlveclem  40284  diblss  40346  pellexlem5  41875  pellex  41877  dvnprodlem1  44962  hoicvr  45564  hoicvrrex  45572  ovn0lem  45581  ovnhoilem1  45617  thincciso  47758