Theorem op1st 7951

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3442  {csn 4582  ⟨cop 4588  ∪ cuni 4865  dom cdm 5632  ‘cfv 6500  1^st c1st 7941

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fv 6508  df-1st 7943

This theorem is referenced by:  op1std  7953  op1stg  7955  1stval2  7960  fo1stres  7969  opreuopreu  7988  eloprabi  8017  xpmapenlem  9084  fseqenlem2  9947  archnq  10903  ruclem8  16174  idfu1st  17815  cofu1st  17819  xpccatid  18123  prf1st  18139  yonedalem21  18208  yonedalem22  18213  2ndcctbss  23411  upxp  23579  uptx  23581  cnheiborlem  24921  ovollb2lem  25457  ovolctb  25459  ovoliunlem2  25472  ovolshftlem1  25478  ovolscalem1  25482  ovolicc1  25485  addsqnreup  27422  2sqreuop  27441  2sqreuopnn  27442  2sqreuoplt  27443  2sqreuopltb  27444  2sqreuopnnlt  27445  2sqreuopnnltb  27446  precsexlem1  28215  precsexlem4  28218  ex-1st  30531  cnnvg  30766  cnnvs  30768  h2hva  31062  h2hsm  31063  hhssva  31345  hhsssm  31346  hhshsslem1  31355  gsumhashmul  33161  rlocf1  33367  fracfld  33402  eulerpartlemgvv  34554  eulerpartlemgh  34556  satfv0fvfmla0  35629  filnetlem3  36596  poimirlem17  37888  heiborlem8  38069  dvhvaddass  41473  dvhlveclem  41484  diblss  41546  aks6d1c3  42493  pellexlem5  43190  pellex  43192  dvnprodlem1  46304  hoicvr  46906  hoicvrrex  46914  ovn0lem  46923  ovnhoilem1  46959  gpgedgvtx0  48421  gpgedgvtx1  48422  gpg3kgrtriex  48449  pgnioedg1  48468  pgnioedg2  48469  pgnioedg3  48470  pgnioedg4  48471  pgnioedg5  48472  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  pgnbgreunbgrlem5lem1  48480  pgnbgreunbgrlem5lem2  48481  pgnbgreunbgrlem5lem3  48482  eloprab1st2nd  49227  swapf1vala  49625  swapf2f1oaALT  49637  swapfcoa  49640  fuco21  49695  fucof21  49706  prcof1  49747  thincciso  49812