Theorem op1st 7939

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3438  {csn 4578  ⟨cop 4584  ∪ cuni 4861  dom cdm 5622  ‘cfv 6490  1^st c1st 7929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fv 6498  df-1st 7931

This theorem is referenced by:  op1std  7941  op1stg  7943  1stval2  7948  fo1stres  7957  opreuopreu  7976  eloprabi  8005  xpmapenlem  9070  fseqenlem2  9933  archnq  10889  ruclem8  16160  idfu1st  17801  cofu1st  17805  xpccatid  18109  prf1st  18125  yonedalem21  18194  yonedalem22  18199  2ndcctbss  23397  upxp  23565  uptx  23567  cnheiborlem  24907  ovollb2lem  25443  ovolctb  25445  ovoliunlem2  25458  ovolshftlem1  25464  ovolscalem1  25468  ovolicc1  25471  addsqnreup  27408  2sqreuop  27427  2sqreuopnn  27428  2sqreuoplt  27429  2sqreuopltb  27430  2sqreuopnnlt  27431  2sqreuopnnltb  27432  precsexlem1  28175  precsexlem4  28178  ex-1st  30468  cnnvg  30702  cnnvs  30704  h2hva  30998  h2hsm  30999  hhssva  31281  hhsssm  31282  hhshsslem1  31291  gsumhashmul  33099  rlocf1  33304  fracfld  33339  eulerpartlemgvv  34482  eulerpartlemgh  34484  satfv0fvfmla0  35556  filnetlem3  36523  poimirlem17  37777  heiborlem8  37958  dvhvaddass  41296  dvhlveclem  41307  diblss  41369  aks6d1c3  42316  pellexlem5  43017  pellex  43019  dvnprodlem1  46132  hoicvr  46734  hoicvrrex  46742  ovn0lem  46751  ovnhoilem1  46787  gpgedgvtx0  48249  gpgedgvtx1  48250  gpg3kgrtriex  48277  pgnioedg1  48296  pgnioedg2  48297  pgnioedg3  48298  pgnioedg4  48299  pgnioedg5  48300  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  pgnbgreunbgrlem5lem1  48308  pgnbgreunbgrlem5lem2  48309  pgnbgreunbgrlem5lem3  48310  eloprab1st2nd  49055  swapf1vala  49453  swapf2f1oaALT  49465  swapfcoa  49468  fuco21  49523  fucof21  49534  prcof1  49575  thincciso  49640