Theorem op1st 7924

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {csn 4571  ⟨cop 4577  ∪ cuni 4854  dom cdm 5611  ‘cfv 6476  1^st c1st 7914

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-iota 6432  df-fun 6478  df-fv 6484  df-1st 7916

This theorem is referenced by:  op1std  7926  op1stg  7928  1stval2  7933  fo1stres  7942  opreuopreu  7961  eloprabi  7990  xpmapenlem  9052  fseqenlem2  9911  archnq  10866  ruclem8  16141  idfu1st  17781  cofu1st  17785  xpccatid  18089  prf1st  18105  yonedalem21  18174  yonedalem22  18179  2ndcctbss  23365  upxp  23533  uptx  23535  cnheiborlem  24875  ovollb2lem  25411  ovolctb  25413  ovoliunlem2  25426  ovolshftlem1  25432  ovolscalem1  25436  ovolicc1  25439  addsqnreup  27376  2sqreuop  27395  2sqreuopnn  27396  2sqreuoplt  27397  2sqreuopltb  27398  2sqreuopnnlt  27399  2sqreuopnnltb  27400  precsexlem1  28140  precsexlem4  28143  ex-1st  30416  cnnvg  30650  cnnvs  30652  h2hva  30946  h2hsm  30947  hhssva  31229  hhsssm  31230  hhshsslem1  31239  gsumhashmul  33033  rlocf1  33232  fracfld  33266  eulerpartlemgvv  34381  eulerpartlemgh  34383  satfv0fvfmla0  35449  filnetlem3  36414  poimirlem17  37677  heiborlem8  37858  dvhvaddass  41136  dvhlveclem  41147  diblss  41209  aks6d1c3  42156  pellexlem5  42866  pellex  42868  dvnprodlem1  45984  hoicvr  46586  hoicvrrex  46594  ovn0lem  46603  ovnhoilem1  46639  gpgedgvtx0  48092  gpgedgvtx1  48093  gpg3kgrtriex  48120  pgnioedg1  48139  pgnioedg2  48140  pgnioedg3  48141  pgnioedg4  48142  pgnioedg5  48143  pgnbgreunbgrlem2lem1  48145  pgnbgreunbgrlem2lem2  48146  pgnbgreunbgrlem2lem3  48147  pgnbgreunbgrlem5lem1  48151  pgnbgreunbgrlem5lem2  48152  pgnbgreunbgrlem5lem3  48153  eloprab1st2nd  48899  swapf1vala  49298  swapf2f1oaALT  49310  swapfcoa  49313  fuco21  49368  fucof21  49379  prcof1  49420  thincciso  49485